Mathlib Map

Theorems · Theorem · group theory

IsUnit.mul

∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit a → IsUnit b → IsUnit (a * b)
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
32 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Commute.isUnit_mul_iff · cited by 9Commute.isUnit_mul_iffIsUnit.mul_iff · cited by 8IsUnit.mul_iffAlgebra.EssFiniteType.comp · cited by 7EssFiniteType.compCStarAlgebra.isStrictlyPositive_TFAE · cited by 7CStarAlgebra.isStrictlyPo…IsUnit.div · cited by 4IsUnit.divUnits.isUnit_units_mul · cited by 4Units.isUnit_units_mulAlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced · cited by 3AlgebraicGeometry.isInteg…IsUnit.div_eq_div_iff · cited by 3IsUnit.div_eq_div_iffIsRelPrime.mul_left · cited by 3IsRelPrime.mul_leftUnits.isUnit_mul_units · cited by 3Units.isUnit_mul_unitsspectrum.units_conjugate · cited by 2spectrum.units_conjugatePowerSeries.IsWeierstrassFactorizationAt.mul · cited by 2IsWeierstrassFactorizatio…PowerSeries.IsWeierstrassFactorizationAt.smul · cited by 2IsWeierstrassFactorizatio…Commute.div_eq_div_iff_of_isUnit · cited by 2Commute.div_eq_div_iff_of…Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map · cited by 2Monic.irreducible_iff_irr…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitIsUnit.mulCITED BYCITES

Cites4

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

Cited by32

Results whose statement or proof uses this declaration.