instAddGroupWithOne — Mathlib

English

X_q is endowed with AddGroupWithOne structure, extending the additive group structure and the natural casts.

Русский

X_q снабжен структурой AddGroupWithOne, расширяющей аддитивную группу и естественные отображения чисел.

LaTeX

$$$X_q\text{ carries an AddGroupWithOne structure compatible with the natural casts and the additive group structure.}$$$

Lean4

instance : AddGroupWithOne (X q) :=
  { inferInstanceAs (Monoid (X q)), inferInstanceAs (AddCommGroup (X q)),
    inferInstanceAs (NatCast (X q)) with
    natCast_zero := by ext <;> simp
    natCast_succ := fun _ ↦ by ext <;> simp
    intCast := fun n => ⟨n, 0⟩
    intCast_ofNat := fun n => by ext <;> simp
    intCast_negSucc := fun n => by ext <;> simp }

Похожие утверждения