Module

RingHom_finiteDimensional_adjoin_range_of_finite_of_forall_mem_range.lean

Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_finiteDimensional_adjoin_range_of_finite_of_forall_mem_range

2 declarations indexed from sourceView source ↗

Module documentation

Ring Hom finite Dimensional adjoin range of finite of forall mem range

Imports3

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.Tactic.Nontriviality

Imported by3

theorem

isIntegral_apply

L28 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.RingHom_finiteDimensional_adjoin_range_of_finite_of_forall_mem_range.SolChiFinField.isIntegral_apply

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_finiteDimensional_adjoin_range_of_finite_of_forall_mem_range
namespace SolChiFinField

Lean source · statement

theorem isIntegral_apply
    {R S A K : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    [CommRing A] [CommRing K] [Algebra A K]
    (χ' : S →+* K) (h : ∀ r : R, χ' (algebraMap R S r) ∈ (algebraMap A K).range) (s : S) :
    IsIntegral A (χ' s)

theorem

finiteDimensional_adjoin_range_of_finite_of_forall_mem_range

L51 ↗

RingHom.finiteDimensional_adjoin_range_of_finite_of_forall_mem_range

Source context 3 commands