English
There is a canonical AddGroupWithOne structure on ℤ√d extending the additive group of ℤ, with the natural embeddings of integers and 1 as the unit.
Русский
Существует каноническая структура AddGroupWithOne на ℤ√d, допускающая дополнительную структуру над ℤ и единицу как элемент тождества.
LaTeX
$$$1_{\\mathbb{Z}\\sqrt{d}} = (1,0).$$$
Lean4
instance addCommGroup : AddCommGroup (ℤ√d) := by
refine { add := (· + ·)
zero := (0 : ℤ√d)
sub := fun a b => a + -b
neg := Neg.neg
nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩)
add_assoc := ?_
zero_add := ?_
add_zero := ?_
neg_add_cancel := ?_
add_comm := ?_ } <;> intros <;> ext <;> simp [add_comm, add_left_comm]
