English
Two AddCommGroupWithOne structures on R are equal if their additive structure and the unit coincide.
Русский
Две структуры AddCommGroupWithOne на R равны, если совпадают их аддитивная структура и единица.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{AddCommGroupWithOne}(R), \\\\ (A\\\\.toAddGroup = B\\\\.toAddGroup) \\\\land (A.\\\\text{one} = B.\\\\text{one}) \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : AddCommGroupWithOne R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_one :
(letI := inst₁;
One.one :
R) =
(letI := inst₂;
One.one)) :
inst₁ = inst₂ := by
have : inst₁.toAddCommGroup = inst₂.toAddCommGroup := AddCommGroup.ext h_add
have : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne := AddGroupWithOne.ext h_add h_one
injection this with _ h_addMonoidWithOne; injection h_addMonoidWithOne
cases inst₁; cases inst₂
congr
