Theorems · Theorem · category theory
Profinite.NobelingProof.GoodProducts.linearIndependentAux
∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (μ : Ordinal.{u}), Profinite.NobelingProof.P I μ- Cited by
- 1 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderWellFoundedLT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- LinearOrderstatement and proof · cited by 8,572
- Ordinalstatement and proof · cited by 1,688
- IsClosedproof · cited by 1,639
- le_of_ltproof · cited by 1,175
- WellFoundedLTstatement and proof · cited by 491
- lt_of_lt_of_leproof · cited by 438
- Order.IsSuccLimitproof · cited by 255
- Ordinal.typeproof · cited by 207
- Profinite.NobelingProof.πproof · cited by 70
- Profinite.NobelingProof.ordproof · cited by 51
- Order.lt_succproof · cited by 45
Cited by1
Results whose statement or proof uses this declaration.
- Profinite.NobelingProof.GoodProducts.linearIndependentproof · cited by 0