Mathlib Map

Theorems · Theorem · ring theory

Unitary.mul_star_self_of_mem

∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → U * star U = 1
Defined in
Mathlib.Algebra.Star.Unitary
Cited by
6 results in Mathlib
Foundations
Depth 22 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.

Unitary.star_mem · cited by 3Unitary.star_memUnitary.coe_mul_star_self · cited by 2Unitary.coe_mul_star_selfUnitary.smul_mem_of_mem · cited by 1Unitary.smul_mem_of_mementry_norm_bound_of_unitary · cited by 1entry_norm_bound_of_unita…Unitary.conjStarAlgAut_ext_iff' · cited by 0Unitary.conjStarAlgAut_ex…Unitary.tmul_mem · cited by 0Unitary.tmul_memMonoid · cited by 3887MonoidSubmonoid · cited by 3086SubmonoidStar.star · cited by 1082Star.starunitary · cited by 207unitaryStarMul · cited by 195StarMulUnitary.mul_star_self_of_memCITED 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
  • Submonoidstatement · cited by 3,086
  • Star.starstatement · cited by 1,082
  • unitarystatement and proof · cited by 207
  • StarMulstatement and proof · cited by 195

Cited by6

Results whose statement or proof uses this declaration.