English
Construct AddGroupWithOne on S using an injective map to R that preserves 0, 1 and addition.
Русский
Построить AddGroupWithOne на S через инъекцию в R, сохраняющую 0, 1 и сложение.
LaTeX
$$AddGroupWithOne S defined via f, preserving 0, 1 and addition.$$
Lean4
/-- A type endowed with `0`, `1` and `+` is an additive commutative monoid with one, if it admits an
injective map that preserves `0`, `1` and `+` to an additive commutative monoid with one.
See note [reducible non-instances]. -/
protected abbrev addCommMonoidWithOne {S} [Zero S] [One S] [Add S] [SMul ℕ S] [NatCast S] [AddCommMonoidWithOne 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)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) : AddCommMonoidWithOne S
where
__ := hf.addMonoidWithOne f zero one add nsmul natCast
__ := hf.addCommMonoid _ zero add (swap nsmul)
