English
Transfer AddGroupWithOne across an Equiv: α inherits AddGroupWithOne from β via e, including integer casting via the inverse map.
Русский
Перенос AddGroupWithOne через эквивалентность: α наследует AddGroupWithOne от β через e, включая целочисленное приведение через обратную карту.
LaTeX
$$$\text{protected abbrev addGroupWithOne } [AddGroupWithOne \beta] : AddGroupWithOne \alpha$$$
Lean4
/-- Transfer `AddGroupWithOne` across an `Equiv` -/
protected abbrev addGroupWithOne [AddGroupWithOne β] : AddGroupWithOne α :=
{ e.addMonoidWithOne, e.addGroup with
intCast := fun n => e.symm n
intCast_ofNat := fun n => by simp only [Int.cast_natCast]; rfl
intCast_negSucc := fun _ =>
congr_arg e.symm <| (Int.cast_negSucc _).trans <| congr_arg _ (e.apply_symm_apply _).symm }
