English
Transfer AddMonoidWithOne across an Equiv: α inherits AddMonoidWithOne structure from β via e, including natural-number casting via the inverse map.
Русский
Перенос AddMonoidWithOne через эквивалентность: α наследует строение AddMonoidWithOne от β через e, включая естественное отображение чисел.
LaTeX
$$$\text{protected abbrev addMonoidWithOne } [AddMonoidWithOne \beta] : AddMonoidWithOne \alpha$$$
Lean4
/-- Transfer `AddMonoidWithOne` across an `Equiv` -/
protected abbrev addMonoidWithOne [AddMonoidWithOne β] : AddMonoidWithOne α :=
{ e.addMonoid, e.one with
natCast := fun n => e.symm n
natCast_zero := e.injective (by simp [zero_def])
natCast_succ := fun n => e.injective (by simp [add_def, one_def]) }
