Theorems · Theorem · ring theory
TrivSqZeroExt.inl_mul
∀ {R : Type u} (M : Type v) [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
[inst_3 : DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R),
TrivSqZeroExt.inl (r₁ * r₂) = TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂- Defined in
- Mathlib.Algebra.TrivSqZeroExt.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- AddMonoidstatement and proof · cited by 2,864
- zero_addproof · cited by 2,366
- MulOppositestatement and proof · cited by 1,135
- smul_zeroproof · cited by 665
- DistribMulActionstatement and proof · cited by 584
- MulOpposite.opproof · cited by 520
- TrivSqZeroExtstatement · cited by 180
- TrivSqZeroExt.inlstatement · cited by 64
- TrivSqZeroExt.extproof · cited by 29
Cited by2
Results whose statement or proof uses this declaration.
- DualNumber.exists_mul_left_or_mul_rightproof · cited by 0
- TrivSqZeroExt.inl_mul_inlproof · cited by 0