Mathlib Map

Theorems · Theorem · ring theory

Units.coe_star

∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (u : Rˣ), ↑(star u) = star ↑u
Defined in
Mathlib.Algebra.Star.Basic
Cited by
2 results in Mathlib
Foundations
Depth 24 from the axioms · uses propext, Quot.sound
Assumes
MonoidStarMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ring.inverse_star · cited by 2Ring.inverse_starIsUnit.isStrictlyPositive_star_right_conjugate_iff · cited by 1IsUnit.isStrictlyPositive…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valStar.star · cited by 1082Star.starStarMul · cited by 195StarMulUnits.coe_starCITED BYCITES

Cites5

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

  • Monoidstatement and proof · cited by 3,887
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement · cited by 1,966
  • Star.starstatement · cited by 1,082
  • StarMulstatement and proof · cited by 195

Cited by2

Results whose statement or proof uses this declaration.