Theorems · Theorem · commutative algebra
FreeCommRing.exists_finite_support
∀ {α : Type u} (x : FreeCommRing α), ∃ s, s.Finite ∧ x.IsSupported s- Defined in
- Mathlib.RingTheory.FreeCommRing
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Finitestatement and proof · cited by 1,814
- Set.mem_singletonproof · cited by 183
- Set.subset_union_leftproof · cited by 142
- Set.subset_union_rightproof · cited by 123
- Set.Finite.unionproof · cited by 74
- Set.finite_singletonproof · cited by 70
- FreeCommRingstatement and proof · cited by 43
- Set.finite_emptyproof · cited by 26
- FreeCommRing.IsSupportedstatement and proof · cited by 12
- FreeCommRing.induction_onproof · cited by 4
- FreeCommRing.isSupported_addproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- FreeCommRing.exists_finset_supportproof · cited by 0