Mathlib Map

Theorems · Theorem · ring theory

IsUnit.star

∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] {a : R}, IsUnit a → IsUnit (star a)
Defined in
Mathlib.Algebra.Star.Basic
Cited by
11 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.

CStarAlgebra.isStrictlyPositive_TFAE · cited by 7CStarAlgebra.isStrictlyPo…isUnit_star · cited by 2isUnit_starIsUnit.isSelfAdjoint_conjugate_iff · cited by 1IsUnit.isSelfAdjoint_conj…Matrix.IsUnit.posDef_star_right_conjugate_iff · cited by 1IsUnit.posDef_star_right_…Matrix.IsUnit.posSemidef_star_right_conjugate_iff · cited by 1IsUnit.posSemidef_star_ri…StarSubalgebra.coe_isUnit · cited by 1StarSubalgebra.coe_isUnitspectrum.star_mem_resolventSet_iff · cited by 1spectrum.star_mem_resolve…IsUnit.mem_unitary_iff_mul_star_self · cited by 1IsUnit.mem_unitary_iff_mu…IsUnit.isSelfAdjoint_conjugate_iff' · cited by 0IsUnit.isSelfAdjoint_conj…IsUnit.isStrictlyPositive_star_left_conjugate_iff · cited by 0IsUnit.isStrictlyPositive…IsUnit.star_left_conjugate_nonneg_iff · cited by 0IsUnit.star_left_conjugat…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitStar.star · cited by 1082Star.starStarMul · cited by 195StarMulIsUnit.starCITED BYCITES

Cites6

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
  • Unitsproof · cited by 2,804
  • Units.valproof · cited by 1,966
  • IsUnitstatement and proof · cited by 1,602
  • Star.starstatement and proof · cited by 1,082
  • StarMulstatement and proof · cited by 195

Cited by11

Results whose statement or proof uses this declaration.