Theorems · Definition · commutative algebra
FreeCommRing.IsSupported
{α : Type u} → FreeCommRing α → Set α → Propis_supported x s means that all monomials showing up in x have variables in s.
- Defined in
- Mathlib.RingTheory.FreeCommRing
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.imageproof · cited by 5,609
- Subring.closureproof · cited by 78
- FreeCommRingstatement and proof · cited by 43
- FreeCommRing.ofproof · cited by 34
Cited by12
Results whose statement or proof uses this declaration.
- FreeCommRing.isSupported_addstatement and proof · cited by 2
- FreeCommRing.isSupported_onestatement · cited by 2
- FreeCommRing.exists_finite_supportstatement and proof · cited by 1
- FreeCommRing.isSupported_mulstatement and proof · cited by 1
- FreeCommRing.isSupported_negstatement and proof · cited by 1
- FreeCommRing.isSupported_ofstatement and proof · cited by 1
- FreeCommRing.isSupported_substatement and proof · cited by 1
- FreeCommRing.isSupported_upwardsstatement and proof · cited by 1
- FreeCommRing.isSupported_zerostatement · cited by 1
- FreeCommRing.exists_finset_supportstatement and proof · cited by 0
- FreeCommRing.isSupported_intstatement and proof · cited by 0
- FreeCommRing.map_subtype_val_restrictionstatement and proof · cited by 0