Mathlib Map

Theorems · Theorem · group theory

Units.val_injective

∀ {α : Type u} [inst : Monoid α], Function.Injective Units.val
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
17 results in Mathlib
Foundations
Depth 10 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.ext · cited by 86Units.extUnits.val_inj · cited by 20Units.val_injorderOf_units · cited by 9orderOf_unitsUnits.coeHom_injective · cited by 4Units.coeHom_injectiveNumberField.Units.coe_injective · cited by 3Units.coe_injectiveFiniteField.unit_isSquare_iff · cited by 2FiniteField.unit_isSquare…card_units_lt · cited by 2card_units_ltUnits.isEmbedding_val_mk' · cited by 2Units.isEmbedding_val_mk'MulChar.sum_one_eq_card_units · cited by 2MulChar.sum_one_eq_card_u…lucas_primality · cited by 2lucas_primalityFiniteField.sum_pow_lt_card_sub_one · cited by 1FiniteField.sum_pow_lt_ca…Units.orderEmbeddingVal · cited by 1Units.orderEmbeddingValreverse_lucas_primality · cited by 1reverse_lucas_primalityLagrange.nodal_subgroup_eq_X_pow_card_sub_one · cited by 0Lagrange.nodal_subgroup_e…MulChar.equivToUnitHom_mul_apply · cited by 0MulChar.equivToUnitHom_mu…Monoid · cited by 3887Monoidmul_one · cited by 3885mul_oneone_mul · cited by 2841one_mulUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valmul_assoc · cited by 1667mul_assocUnits.val_injectiveCITED 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
  • mul_oneproof · cited by 3,885
  • one_mulproof · cited by 2,841
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement and proof · cited by 1,966
  • mul_assocproof · cited by 1,667

Cited by18

Results whose statement or proof uses this declaration.