English
Pull back AddCommGroupWithOne along an injective map preserving 0,1 and addition, obtaining a compatible structure on the domain.
Русский
Через инъекцию переносимую структуру AddCommGroupWithOne получаем на области определение.
LaTeX
$$AddCommGroupWithOne S obtained by pulling back f along hf.$$
Lean4
/-- A type endowed with `0`, `1` and `+` is an additive group with one, if it admits an injective
map that preserves `0`, `1` and `+` to an additive group with one. See note
[reducible non-instances]. -/
protected abbrev addGroupWithOne {S} [Zero S] [One S] [Add S] [SMul ℕ S] [Neg S] [Sub S] [SMul ℤ S] [NatCast S]
[IntCast S] [AddGroupWithOne R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
(add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
(natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : AddGroupWithOne S :=
{ hf.addGroup f zero add neg sub (swap nsmul) (swap zsmul), hf.addMonoidWithOne f zero one add nsmul natCast with
intCast := Int.cast, intCast_ofNat := fun n => hf (by rw [natCast, intCast, Int.cast_natCast]),
intCast_negSucc := fun n => hf (by rw [intCast, neg, natCast, Int.cast_negSucc]) }
