Module

Algebra_QuasiFinite_of_flat_of_quasiFinite_genericFiber.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_QuasiFinite_of_flat_of_quasiFinite_genericFiber

1 declaration indexed from sourceView source ↗

Module documentation

Algebra Quasi Finite of flat of quasi Finite generic Fiber

Imports11

Mathlib.RingTheory.QuasiFinite.Basic
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem

Imported by2

theorem

of_flat_of_quasiFinite_genericFiber

L36 ↗

Algebra.QuasiFinite.of_flat_of_quasiFinite_genericFiber

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_QuasiFinite_of_flat_of_quasiFinite_genericFiber
open scoped TensorProduct

Lean source · statement

theorem _root_.Algebra.QuasiFinite.of_flat_of_quasiFinite_genericFiber
    {R B K : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.DimensionLEOne R]
    [CommRing B] [Algebra R B] [Module.Flat R B] [Algebra.FiniteType R B]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (hgen : Algebra.QuasiFinite K (K ⊗[R] B)) : Algebra.QuasiFinite R B

Module documentation

Algebra Quasi Finite of flat of quasi Finite generic Fiber

Declarations

of_flat_of_quasiFinite_genericFiber