Namespace Subring 10 theorems
- Orders in ℂ embed into complete DVRs above ℓ
Subring.exists_injective_ringHom_isDiscreteValuationRing_of_module_finite0 below · cited by 1 · depth 9 - Orders in ℂ embed into complete DVRs respecting a prime above l
Subring.exists_injective_ringHom_isDiscreteValuationRing_map_mem_maximalIdeal_of_module_finite0 below · cited by 1 · depth 13 - Locality of integral subrings via marked Galois descent
Subring.eq_of_isMaximal_of_marked_galois_descent1 below · cited by 1 · depth 20 - Primes of O[B] over mathfrak m_O are maximal
Subring.isMaximal_of_liesOver_adjoin_of_forall_not_isMaximal_valuationSubring1 below · cited by 2 · depth 27 - A two-sided quasi-inverse of a centralising element centralises
Subring.mem_centralizer_of_mul_eq_of_mul_eq_of_forall_mul_eq_mul0 below · cited by 3 · depth 28 - An integrally closed subring with fraction field F absorbs integral over-rings
Subring.eq_of_le_of_forall_isIntegral_of_isIntegrallyClosed0 below · cited by 1 · depth 30 - An invariant element regular on a finite family, with a pole along V
Subring.exists_forall_algEquiv_apply_eq_and_forall_mem_and_not_mem_valuationSubring1 below · cited by 3 · depth 30 - Directed union of Noetherian local rings along flat inclusions
Subring.exists_isLocalRing_isNoetherianRing_faithfullyFlat_of_directed_of_flat_of_map_maximalIdeal_eq0 below · cited by 1 · depth 34 - Localisation at a maximal ideal inside a field: completion unchanged
Subring.exists_isLocalRing_ringEquiv_adicCompletion_of_forall_mem_iff_exists_mul_eq_of_isMaximal0 below · cited by 4 · depth 34 - A valuation subring of ̄ K cutting out kerψ
Subring.exists_valuationSubring_mem_maximalIdeal_iff_apply_eq_zero0 below · cited by 2 · depth 38