Documentation Verification Report

Norm

📁 Source: Mathlib/RingTheory/FractionalIdeal/Norm.lean

Statistics

Metric	Count
Definitions `absNorm`, `Norm`	2
Theorems `absNorm_bot`, `absNorm_div_norm_eq_absNorm_div_norm`, `absNorm_eq`, `absNorm_eq'`, `absNorm_eq_zero_iff`, `absNorm_nonneg`, `absNorm_one`, `absNorm_span_singleton`, `abs_det_basis_change`, `coeIdeal_absNorm`	10
Total	12

FractionalIdeal

Definitions

Name	Category	Theorems
`absNorm` 📖	CompOp	14 math math: `absNorm_eq'`, `NumberField.det_basisOfFractionalIdeal_eq_absNorm`, `absNorm_bot`, `NumberField.mixedEmbedding.covolume_idealLattice`, `NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm`, `absNorm_eq`, `absNorm_span_singleton`, `NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis`, `absNorm_nonneg`, `abs_det_basis_change`, `NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr`, `coeIdeal_absNorm`, `absNorm_eq_zero_iff`, `absNorm_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_bot` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `orderBot`	—	`ZeroHom.map_zero'`
`absNorm_div_norm_eq_absNorm_div_norm` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `coeToSubmodule` `Submodule.map` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Algebra.linearMap`	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `num` `abs` `instLatticeInt` `Int.instAddGroup` `MonoidHom` `MulOneClass.toMulOne` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `den`	—	`smulCommClass_self` `RingHomSurjective.ids` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `div_eq_div_iff` `Int.cast_abs` `Rat.instIsStrictOrderedRing` `Rat.instAddLeftMono` `covariant_swap_add_of_covariant_add` `Rat.instCharZero` `Int.instIsDomain` `den_mul_self_eq_num` `IsScalarTower.right` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `mul_comm` `smul_eq_mul` `IsScalarTower.left` `LinearMap.map_injective` `LinearMap.ker_eq_bot` `IsFractionRing.injective` `Submodule.map_smul''` `Submodule.ideal_span_singleton_smul` `Submonoid.smul_def` `SMulCommClass.smul_comm` `Submonoid.smulCommClass_left` `Submonoid.smulCommClass_right`
`absNorm_eq` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `num` `abs` `instLatticeInt` `Int.instAddGroup` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Ring.toSemiring` `CommRing.toRing` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `den`	—	—
`absNorm_eq'` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `coeToSubmodule` `Submodule.map` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Algebra.linearMap`	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `NonAssocSemiring.toMulZeroOneClass` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `abs` `instLatticeInt` `Int.instAddGroup` `MonoidHom` `MulOneClass.toMulOne` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra`	—	`smulCommClass_self` `RingHomSurjective.ids` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `absNorm.eq_1` `absNorm_div_norm_eq_absNorm_div_norm`
`absNorm_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `instZero`	—	`zero_of_num_eq_bot` `IsDedekindDomain.toIsDomain` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero` `zero_notMem_nonZeroDivisors` `Ideal.absNorm_eq_zero_iff` `Nat.cast_eq_zero` `Rat.instCharZero` `div_eq_zero_iff` `absNorm_eq` `Int.cast_abs` `Rat.instIsStrictOrderedRing` `Rat.instAddLeftMono` `covariant_swap_add_of_covariant_add` `Int.instIsDomain` `absNorm_bot`
`absNorm_nonneg` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm`	—	`div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `Nat.cast_nonneg'` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Int.cast_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `abs_nonneg` `Int.instAddLeftMono` `covariant_swap_add_of_covariant_add`
`absNorm_one` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `instOne`	—	`MonoidWithZeroHom.map_one'`
`absNorm_span_singleton` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `spanSingleton` `abs` `Rat.instLattice` `Rat.addGroup` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Ring.toSemiring` `CommRing.toRing` `Rat.commRing` `MonoidHom.instFunLike` `Algebra.norm`	—	`IsFractionRing.isDomain` `IsDedekindDomain.toIsDomain` `IsLocalization.exists_integer_multiple` `IsDomain.toNontrivial` `absNorm_eq'` `Submodule.ext` `smulCommClass_self` `RingHomSurjective.ids` `Submonoid.smulCommClass_left` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `SMulCommClass.smul_comm` `Ideal.absNorm_span_singleton` `Nat.cast_natAbs` `Int.cast_abs` `Rat.instIsStrictOrderedRing` `Algebra.norm_localization` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `Algebra.smul_def` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `abs_mul` `IsStrictOrderedRing.toIsOrderedRing` `mul_div_assoc` `mul_div_cancel₀` `abs_eq_zero` `Rat.instAddLeftMono` `covariant_swap_add_of_covariant_add` `Algebra.norm_eq_zero_iff` `Rat.isDomain` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsFractionRing.to_map_eq_zero_iff` `nonZeroDivisors.coe_ne_zero`
`abs_det_basis_change` 📖	mathematical	—	`abs` `Rat.instLattice` `Rat.addGroup` `DFunLike.coe` `AlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rat.commRing` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.toModule` `Rat.commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `AlternatingMap.instFunLike` `Module.Basis.det` `Module.Basis.localizationLocalization` `Int.instCommSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Int.instSemiring` `Ring.toIntAlgebra` `DivisionRing.toRing` `Rat.instDivisionRing` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `Submodule` `SetLike.instMembership` `Submodule.setLike` `coeToSubmodule` `Module.Basis` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `Module.Basis.instFunLike` `MonoidWithZeroHom` `FractionalIdeal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm`	—	`IsFractionRing.nontrivial` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `LinearMap.CompatibleSMul.intModule` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toIsCancelMulZero` `nonZeroDivisors.coe_ne_zero` `absNorm_eq` `Ideal.natAbs_det_basis_change` `Nat.cast_natAbs` `Int.cast_abs` `Rat.instIsStrictOrderedRing` `Module.Basis.det_apply` `RingHom.map_det` `Matrix.ext` `RingHomInvPair.ids` `Module.Basis.localizationLocalization_repr_algebraMap` `equivNum_apply` `Algebra.smul_def` `Module.Basis.toMatrix_smul` `Matrix.det_mul` `abs_mul` `IsStrictOrderedRing.toIsOrderedRing` `Algebra.norm_eq_matrix_det` `Algebra.norm_localization` `mul_div_assoc` `mul_div_cancel₀` `abs_eq_zero` `Rat.instAddLeftMono` `covariant_swap_add_of_covariant_add` `IsFractionRing.to_map_eq_zero_iff` `Algebra.norm_eq_zero_iff_of_basis` `Finite.of_fintype` `Int.instIsDomain`
`coeIdeal_absNorm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `absNorm` `coeIdeal` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `absNorm_eq'` `smulCommClass_self` `RingHomSurjective.ids` `one_smul` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `OneMemClass.coe_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.cast_one` `div_one`

(root)

Definitions

Name	Category	Theorems
`Norm` 📖	CompData	—

---

← Back to Index