English
Let R be a type and A,B two AddCommMonoidWithOne-structures on R. If A and B have the same additive operation and the same unit element 1, then A and B are equal.
Русский
Пусть R — тип, A и B — структуры AddCommMonoidWithOne на R. Если у них совпадают операция сложения и единица 1, то структуры совпадают.
LaTeX
$$$\\\\forall R \, \\, \\forall A,B \in \\text{AddCommMonoidWithOne}(R), \\\\ (+)_A = (+)_B \\\\land 1_A = 1_B \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : AddCommMonoidWithOne R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_one :
(letI := inst₁;
One.one :
R) =
(letI := inst₂;
One.one :
R)) :
inst₁ = inst₂ :=
AddCommMonoidWithOne.toAddMonoidWithOne_injective <| AddMonoidWithOne.ext h_add h_one
