Theorems · Definition · ring theory
StarAlgHom.ofId
(R : Type u_7) →
(A : Type u_8) →
[inst : CommSemiring R] →
[inst_1 : StarRing R] →
[inst_2 : Semiring A] → [inst_3 : StarMul A] → [inst_4 : Algebra R A] → [StarModule R A] → R →⋆ₐ[R] AalgebraMap R A as a StarAlgHom when A is a star algebra over R.
- Defined in
- Mathlib.Algebra.Star.StarAlgHom
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Algebra.algebraMapproof · cited by 4,706
- AlgHomproof · cited by 3,236
- StarRingstatement and proof · cited by 1,686
- StarModulestatement and proof · cited by 570
- StarAlgHomstatement · cited by 215
- StarMulstatement and proof · cited by 195
- Algebra.ofIdproof · cited by 166
Cited by21
Results whose statement or proof uses this declaration.
- QuasispectrumRestricts.nonUnitalStarAlgHomproof · cited by 10
- SpectrumRestricts.starAlgHomproof · cited by 10
- StarAlgHom.ofId_applystatement and proof · cited by 6
- QuasispectrumRestricts.nonUnitalStarAlgHom_applystatement · cited by 4
- SpectrumRestricts.starAlgHom_applystatement · cited by 4
- QuasispectrumRestricts.cfcproof · cited by 2
- QuasispectrumRestricts.cfcₙ_eq_restrictproof · cited by 2
- QuasispectrumRestricts.continuous_nonUnitalStarAlgHomproof · cited by 2
- SpectrumRestricts.cfcproof · cited by 2
- SpectrumRestricts.cfc_eq_restrictproof · cited by 2
- SpectrumRestricts.continuous_starAlgHomproof · cited by 2
- QuasispectrumRestricts.nonUnitalStarAlgHom_idproof · cited by 2