English
Under surjective f and AddMonoidWithOne on the domain, the codomain inherits an AddMonoidWithOne structure compatibly.
Русский
При сюръекции f и наличии AddMonoidWithOne в области определения, кодомоноидная единица переносится на область значений.
LaTeX
$$$\\forall n\\in\\mathbb{N}, f(n)=n,$$$
Lean4
/-- A type endowed with `0`, `1` and `+` is an additive monoid with one,
if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one.
See note [reducible non-instances]. -/
protected abbrev addCommMonoidWithOne [AddCommMonoidWithOne R] (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)
