Theorems · Theorem · commutative algebra
Ideal.sub_mem
∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a b : α}, a ∈ I → b ∈ I → a - b ∈ I- Defined in
- Mathlib.RingTheory.Ideal.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Idealstatement and proof · cited by 4,748
- Submodule.sub_memproof · cited by 43
Cited by22
Results whose statement or proof uses this declaration.
- Ideal.map_isPrime_of_surjectiveproof · cited by 11
- PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_modproof · cited by 10
- Algebra.Generators.Cotangent.exactproof · cited by 6
- Ideal.Quotient.maximal_of_isFieldproof · cited by 4
- Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_memproof · cited by 3
- Ideal.cotangent_subsingleton_iffproof · cited by 3
- Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulproof · cited by 3
- Ideal.mem_jacobson_iffproof · cited by 2
- DividedPowers.isSubDPIdeal_inf_iffproof · cited by 2
- IsAdic.isPrecomplete_iffproof · cited by 2
- IsAdicComplete.le_jacobson_botproof · cited by 1
- PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrimeproof · cited by 1