Commit 2024-01-09 09:24 2a950180

View on Github →

feat: Define intNorm and intTrace. (#9265)

Estimated changes

Modified Mathlib/RingTheory/IntegralRestrict.lean

added theorem Algebra.algebraMap_intNorm

added theorem Algebra.algebraMap_intNorm_fractionRing

added theorem Algebra.algebraMap_intNorm_of_isGalois

added theorem Algebra.algebraMap_intTrace

added theorem Algebra.algebraMap_intTrace_fractionRing

added def Algebra.intNorm

added def Algebra.intNormAux

added theorem Algebra.intNorm_eq_norm

added theorem Algebra.intNorm_eq_of_isLocalization

added theorem Algebra.intNorm_eq_zero

added theorem Algebra.intNorm_ne_zero

added theorem Algebra.intNorm_zero

added def Algebra.intTrace

added def Algebra.intTraceAux

added theorem Algebra.intTrace_eq_of_isLocalization

added theorem Algebra.intTrace_eq_trace

added theorem Algebra.map_intNormAux

added theorem Algebra.map_intTraceAux

Modified Mathlib/RingTheory/LocalProperties.lean

added theorem Module.Finite_of_isLocalization

Modified Mathlib/RingTheory/Localization/Integral.lean

added theorem isAlgebraic_of_isFractionRing

added theorem isAlgebraic_of_isLocalization