feat: add StarAlgHom.ofId (#8993)

leanprover-community · Dec 12, 2023 · cc5a723 · cc5a723
1 parent 15f6474
commit cc5a723
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean
@@ -450,6 +450,14 @@ theorem coe_id : ⇑(StarAlgHom.id R A) = id :=
   rfl
 #align star_alg_hom.coe_id StarAlgHom.coe_id
 
+/-- `algebraMap R A` as a `StarAlgHom` when `A` is a star algebra over `R`. -/
+@[simps]
+def ofId (R A : Type*) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A]
+    [Algebra R A] [StarModule R A] : R →⋆ₐ[R] A :=
+  { Algebra.ofId R A with
+    toFun := algebraMap R A
+    map_star' := by simp [Algebra.algebraMap_eq_smul_one] }
+
 end
 
 instance : Inhabited (A →⋆ₐ[R] A) :=