zero_smul
theorem zero_smul :
∀ (R : Type u_1) {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M), 0 • m = 0
This theorem, `zero_smul`, states that for any type `R` with a zero element, and any type `M` also with a zero element, if `R` and `M` form a scalar multiplication structure with zero (`SMulWithZero`), then scalar multiplication of any element `m` of type `M` by the zero of `R` results in the zero of `M`. In mathematical terms, if we can multiply elements of `R` with elements of `M` in a way that respects zero, then 0 times any element is always zero.
More concisely: For types `R` and `M` with zero elements, if `R` and `M` have a scalar multiplication structure with zero then multiplication by the zero of `R` results in the zero of `M`.
|
MulActionWithZero.smul_zero
theorem MulActionWithZero.smul_zero :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M] (r : R),
r • 0 = 0
The theorem `MulActionWithZero.smul_zero` states that for any types `R` and `M`, where `R` is a type with monoid with zero structure, `M` is a type with zero structure, and there is a scalar multiplication action defined between `R` and `M` (represented as `MulActionWithZero R M`), the scalar multiplication of any element of `R` (denoted by `r`) and the zero element of `M` always results in the zero element of `M`. In other words, for all `r` in `R`, `r • 0 = 0`. This is a generalization of the familiar property in linear algebra where multiplying any scalar with the zero vector results in the zero vector.
More concisely: For any types `R` and `M` with monoid and zero structures, and a scalar multiplication action `MulActionWithZero R M`, the scalar multiplication of any element in `R` with the zero element in `M` results in the zero element in `M`.
|
SMulWithZero.zero_smul
theorem SMulWithZero.zero_smul :
∀ {R : Type u_1} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [self : SMulWithZero R M] (m : M), 0 • m = 0 := by
sorry
This theorem states that for any types `R` and `M`, where `R` has a zero element and `M` also has a zero element, and there is a scalar multiplication operation defined with zero in `R` on `M`, the scalar multiplication of any element of `M` by the zero of `R` results in the zero of `M`. In mathematical terms, it says that for `m` in `M`, `0 * m = 0`.
More concisely: For any type `M` with zero element, and given a scalar multiplication operation from a type `R` with zero element, the scalar multiplication of any element in `M` by the zero of `R` yields the zero element in `M`.
|
MulActionWithZero.zero_smul
theorem MulActionWithZero.zero_smul :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M] (m : M),
0 • m = 0
The theorem `MulActionWithZero.zero_smul` states that for any types `R` and `M`, where `R` is a monoid with zero and `M` is a type with a zero element, and given a multiplication action of `R` on `M` with respect to the zero element, scalar multiplication of any element `m` of `M` by the zero scalar from `R` results in the zero element of `M`. In simpler terms, multiplying any element by zero results in zero.
More concisely: For any monoid `R` with zero and type `M` with a zero element, the scalar multiplication of any element `m` in `M` by the zero scalar in `R` results in the zero element of `M`. In other words, 0 * m = 0 for all m in M.
|