Mathlib Map

Theorems · Theorem · ring theory

Unitization.inr_star

∀ {R : Type u_1} {A : Type u_2} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] (a : A),
  ↑(star a) = star ↑a
Defined in
Mathlib.Algebra.Algebra.Unitization
Cited by
3 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Quot.sound
Assumes
AddMonoidStarAddMonoidStar
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SemiconjBy.star_right · cited by 2SemiconjBy.star_rightCStarAlgebra.star_left_conjugate_le_norm_smul · cited by 1CStarAlgebra.star_left_co…CStarAlgebra.spectralOrderedRing · cited by 1CStarAlgebra.spectralOrde…AddMonoid · cited by 2864AddMonoidStar.star · cited by 1082Star.starStar · cited by 496StarStarAddMonoid · cited by 296StarAddMonoidUnitization · cited by 220UnitizationUnitization.inr · cited by 109Unitization.inrstar_zero · cited by 58star_zeroUnitization.ext · cited by 21Unitization.extUnitization.inr_starCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.