instAddGroupWithOne — Mathlib

English

The product of AddGroupWithOne structures carries a natural additive-one structure, with integer casting defined diagonally: intCast(n) = (n,n).

Русский

Произведение структур AddGroupWithOne на α×β обладает естественной структурой AddGroupWithOne, где целочисленный каст задаётся как диагональ: intCast(n)=(n,n).

LaTeX

$${α: Type*, β: Type*} → [AddGroupWithOne α] → [AddGroupWithOne β] → AddGroupWithOne (Prod α β)$$

Lean4

instance : AddGroupWithOne (α × β) :=
  { Prod.instAddMonoidWithOne,
    Prod.instAddGroup with
    intCast := fun n => (n, n)
    intCast_ofNat := fun _ => by ext <;> simp
    intCast_negSucc := fun _ => by ext <;> simp }

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