Module

Scheme_Hom_natCard_le_finrank_of_isFinite.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_natCard_le_finrank_of_isFinite

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom nat Card le finrank of is Finite

Imports2

Mathlib.RingTheory.Artinian.Module
Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

natCard_primeSpectrum_le_finrank

L30 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_natCard_le_finrank_of_isFinite.MVIneqK12.natCard_primeSpectrum_le_finrank

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_natCard_le_finrank_of_isFinite
universe u
open CategoryTheory AlgebraicGeometry
namespace MVIneqK12

Lean source · statement

theorem natCard_primeSpectrum_le_finrank (k : Type u) [Field k] (A : Type u) [CommRing A] [Algebra
  k A]
    [Module.Finite k A] : Nat.card (PrimeSpectrum A) ≤ Module.finrank k A

theorem

natCard_le_finrank_of_isFinite

L59 ↗

AlgebraicGeometry.Scheme.Hom.natCard_le_finrank_of_isFinite