starCenterIsoCentroid — Mathlib

Lean4

/-- The canonical isomorphism from the center of a (non-associative) semiring onto its centroid. -/
def starCenterIsoCentroid : StarSubsemiring.center α ≃⋆+* CentroidHom α
    where
  __ := starCenterToCentroid
  invFun T := ⟨T 1, by constructor <;> simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]⟩
  left_inv
    z :=
    Subtype.ext <| by
      simp only [MulHom.toFun_eq_coe, NonUnitalRingHom.coe_toMulHom, NonUnitalStarRingHom.coe_toNonUnitalRingHom,
        starCenterToCentroid_apply, mul_one]
  right_inv T := CentroidHom.ext <| fun _ => by simp [starCenterToCentroid_apply, ← map_mul_right]

Похожие утверждения