Theorems · Theorem · commutative algebra
Subring.mul_mem
∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ sA subring is closed under multiplication.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext
- Assumes
- NonAssocRing
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.
- Subringstatement and proof · cited by 602
- NonAssocRingstatement and proof · cited by 483
- MulMemClass.mul_memproof · cited by 173
Cited by7
Results whose statement or proof uses this declaration.
- RingHom.IsIntegralElem.mulproof · cited by 4
- Algebra.adjoin_eq_ring_closureproof · cited by 2
- FreeCommRing.isSupported_mulproof · cited by 1
- IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expCharproof · cited by 1
- Polynomial.mem_closure_X_union_Cproof · cited by 1
- LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMapproof · cited by 1
- ValuationSubring.mul_memproof · cited by 1