Theorems · Theorem · group theory
associated_one_iff_isUnit
∀ {M : Type u_1} [inst : Monoid M] {a : M}, Associated a 1 ↔ IsUnit a- Defined in
- Mathlib.Algebra.GroupWithZero.Associated
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- one_mulproof · cited by 2,841
- Unitsproof · cited by 2,804
- Units.valproof · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- Associatedstatement and proof · cited by 296
- Associated.symmproof · cited by 87
Cited by14
Results whose statement or proof uses this declaration.
- minpoly.eq_of_irreducible_of_monicproof · cited by 9
- isUnit_gcd_of_eq_mul_gcdproof · cited by 3
- exists_associated_pow_of_mul_eq_powproof · cited by 3
- UniqueFactorizationMonoid.radical_of_isUnitproof · cited by 3
- LinearMap.associated_det_of_eq_compproof · cited by 2
- prime_factors_irreducibleproof · cited by 2
- UniqueFactorizationMonoid.factors_of_isUnitproof · cited by 1
- Multiset.extract_gcd'proof · cited by 1
- IsAdjoinRootMonic.minpoly_eqproof · cited by 1
- WfDvdMonoid.of_exists_prime_factorsproof · cited by 1
- Finset.extract_gcd'proof · cited by 1
- Associates.mk_eq_oneproof · cited by 0