Theorems · Theorem · commutative algebra
DivisorChain.first_of_chain_isUnit
∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {q : Associates M} {n : ℕ}
{c : Fin (n + 1) → Associates M}, StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → IsUnit (c 0)- Defined in
- Mathlib.RingTheory.ChainOfDivisors
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitstatement · cited by 1,602
- CommMonoidWithZerostatement and proof · cited by 913
- StrictMonostatement and proof · cited by 706
- Associatesstatement and proof · cited by 210
- IsCancelMulZerostatement and proof · cited by 177
- StrictMono.monotoneproof · cited by 118
- one_leproof · cited by 23
- Associates.isUnit_iff_eq_oneproof · cited by 6
- Associates.le_one_iffproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- DivisorChain.second_of_chain_is_irreducibleproof · cited by 3
- DivisorChain.eq_second_of_chain_of_prime_dvdproof · cited by 1