English
Equality of two monoid structures on the same carrier is a tautology; hence the congruence principle holds for TrivSqZeroExt.
Русский
Равенство двух моноидальных структур над одной носительной структурой есть тавтология; следовательно, конгруэнтность сохраняется для TrivSqZeroExt.
LaTeX
$$$ TrivSqZeroExt.monoid = TrivSqZeroExt.monoid$$$
Lean4
instance commMonoid [CommMonoid R] [AddCommMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
[IsCentralScalar R M] : CommMonoid (tsze R M) :=
{ TrivSqZeroExt.monoid with
mul_comm := fun x₁ x₂ =>
ext (mul_comm x₁.1 x₂.1) <|
show x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1 by
rw [op_smul_eq_smul, op_smul_eq_smul, add_comm] }
