Norm

📁 Source: Mathlib/NumberTheory/NumberField/Norm.lean

Statistics

Metric	Count
Definitions norm	1
Theorems coe_norm_int, coe_trace_int, algebraMap_norm_algebraMap, coe_algebraMap_norm, coe_norm, dvd_norm, isUnit_norm, isUnit_norm_of_isGalois, norm_algebraMap, norm_norm	10
Total	11

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_norm_int 📖	mathematical	—	DFunLike.coe MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing NumberField.RingOfIntegers.instCommRing CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MonoidHom.instFunLike norm Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing Rat.commRing DivisionRing.toRatAlgebra NumberField.to_charZero NumberField.RingOfIntegers.val	—	NumberField.to_charZero norm_localization Rat.isFractionRing NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors AddCommGroup.intIsScalarTower NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt
coe_trace_int 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing RingHom.id Semiring.toNonAssocSemiring NumberField.RingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing toModule Ring.toIntAlgebra CommRing.toRing Semiring.toModule LinearMap.instFunLike trace Rat.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.RingOfIntegers.val	—	NumberField.to_charZero trace_localization Rat.isFractionRing NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors AddCommGroup.intIsScalarTower NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt

RingOfIntegers

Definitions

Name	Category	Theorems
norm 📖	CompOp	9 math math: isUnit_norm_of_isGalois, norm_algebraMap, norm_norm, isUnit_norm, coe_norm, NumberField.isUnit_iff_norm, algebraMap_norm_algebraMap, coe_algebraMap_norm, dvd_norm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_norm_algebraMap 📖	mathematical	—	DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike norm NumberField.inst_ringOfIntegersAlgebra Ring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.norm	—	—
coe_algebraMap_norm 📖	mathematical	—	NumberField.RingOfIntegers.val DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.inst_ringOfIntegersAlgebra MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike norm Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.norm	—	—
coe_norm 📖	mathematical	—	NumberField.RingOfIntegers.val DFunLike.coe MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing MonoidHom.instFunLike norm Ring.toSemiring DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.norm	—	—
dvd_norm 📖	mathematical	—	NumberField.RingOfIntegers semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap NumberField.inst_ringOfIntegersAlgebra MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike norm	—	IsIntegral.prod IsIntegral.map AddCommGroup.intIsScalarTower AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass NumberField.RingOfIntegers.isIntegral_coe NumberField.RingOfIntegers.ext coe_algebraMap_norm Algebra.norm_eq_prod_automorphisms Finset.mul_prod_erase Finset.mem_univ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
isUnit_norm 📖	mathematical	—	IsUnit NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike norm	—	AlgebraicClosure.instIsScalarTower IsScalarTower.right IsScalarTower.left isUnit_pow_iff pos_iff_ne_zero Nat.instCanonicallyOrderedAdd Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing FiniteDimensional.right normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure normalClosure.is_finiteDimensional instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass norm_norm norm_algebraMap map_pow MonoidHom.instMonoidHomClass isUnit_norm_of_isGalois IsGalois.normalClosure IsSepClosure.isGalois IsSepClosure.of_isAlgClosure_of_perfectField AlgebraicClosure.instIsAlgClosureOfIsAlgebraic Algebra.IsSeparable.isAlgebraic Algebra.IsSeparable.of_integral Algebra.IsIntegral.of_finite PerfectField.ofCharZero IsGalois.tower_top_of_isGalois
isUnit_norm_of_isGalois 📖	mathematical	—	IsUnit NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike norm	—	IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_of_mul_isUnit_right instIsDedekindFiniteMonoid prod_mem SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass IsIntegral.map AddCommGroup.intIsScalarTower AlgHom.algHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass NumberField.RingOfIntegers.ext Finset.prod_singleton AlgEquiv.coe_refl NumberField.RingOfIntegers.coe_eq_algebraMap map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Finset.prod_sdiff Finset.subset_univ Algebra.norm_eq_prod_automorphisms coe_algebraMap_norm MonoidHom.instMonoidHomClass
norm_algebraMap 📖	mathematical	—	DFunLike.coe MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing MonoidHom.instFunLike norm RingHom RingHom.instFunLike algebraMap NumberField.inst_ringOfIntegersAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	—	NumberField.RingOfIntegers.ext_iff NumberField.RingOfIntegers.coe_eq_algebraMap algebraMap_norm_algebraMap Algebra.norm_algebraMap map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
norm_norm 📖	mathematical	—	DFunLike.coe MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing MonoidHom.instFunLike norm	—	NumberField.RingOfIntegers.ext_iff coe_norm Algebra.norm_norm Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors

---

← Back to Index