centerIsoCentroid — Mathlib

Lean4
/-- The canonical isomorphism from the center of a (non-associative) semiring onto its centroid. -/
def centerIsoCentroid : Subsemiring.center α ≃+* CentroidHom α :=
  {
    centerToCentroid with
    invFun := fun T ↦ ⟨T 1, by constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]⟩
    left_inv := fun z ↦
      Subtype.ext <| by simp only [MulHom.toFun_eq_coe, NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, mul_one]
    right_inv := fun T ↦
      CentroidHom.ext <| fun _ => by
        rw [MulHom.toFun_eq_coe, NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul] }
Похожие утверждения