addEquiv — Mathlib

Lean4
/-- `Finsupp.mapRange.AddMonoidHom` as an equiv. -/
@[simps apply]
def addEquiv (f : M ≃+ N) : (α →₀ M) ≃+ (α →₀ N) :=
  {
    mapRange.addMonoidHom
      f.toAddMonoidHom with
    toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
    invFun := (mapRange f.symm f.symm.map_zero : (α →₀ N) → α →₀ M)
    left_inv := fun x => by
      rw [← mapRange_comp] <;> simp_rw [AddEquiv.symm_comp_self]
      · exact mapRange_id _
      · rfl
    right_inv := fun x => by
      rw [← mapRange_comp] <;> simp_rw [AddEquiv.self_comp_symm]
      · exact mapRange_id _
      · rfl }
Похожие утверждения