Ideal.under_eq_bot_of_mem_minimalPrimes_of_flat
The contraction of a minimal prime along a flat algebra over a domain is the zero ideal.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Ideal
universe u vLean source · statement
theorem under_eq_bot_of_mem_minimalPrimes_of_flat
{R : Type u} {S : Type v}
[CommRing R] [CommRing S] [Algebra R S]
[IsDomain R] [Module.Flat R S]
(Q : Ideal S) (hQ : Q ∈ minimalPrimes S) :
Q.under R = ⊥