Mathlib Map

Theorems · Theorem · group theory

Units.val_mul

∀ {α : Type u} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑b
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
22 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.

Units.coeHom · cited by 44Units.coeHomAssociated.trans · cited by 22Associated.transMatrix.det_fromBlocks_zero₂₁ · cited by 10Matrix.det_fromBlocks_zer…ZMod.val_coe_unit_coprime · cited by 6ZMod.val_coe_unit_coprimeValuation.subgroups_basis · cited by 5Valuation.subgroups_basisUnits.isUnit_units_mul · cited by 4Units.isUnit_units_mulSubmodule.fg_unit · cited by 3Submodule.fg_unitUnits.isUnit_mul_units · cited by 3Units.isUnit_mul_unitsNormedRing.inverse_add · cited by 2NormedRing.inverse_addClassGroup.mk_eq_mk_of_coe_ideal · cited by 2ClassGroup.mk_eq_mk_of_co…Ring.mul_inverse_rev' · cited by 2Ring.mul_inverse_rev'WeierstrassCurve.coe_inv_variableChange_Δ' · cited by 1WeierstrassCurve.coe_inv_…OreLocalization.universalMulHom_unique · cited by 1OreLocalization.universal…Matrix.rank_unit · cited by 1Matrix.rank_unitPowerSeries.invOneSubPow_eq_inv_one_sub_pow · cited by 1PowerSeries.invOneSubPow_…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valUnits.val_mulCITED BYCITES

Cites3

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

Cited by23

Results whose statement or proof uses this declaration.