Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `norm`	1
Theorems `norm_algebraMap`, `norm_algebraMap_of_basis`, `norm_apply`, `norm_eq_matrix_det`, `norm_eq_one_of_not_exists_basis`, `norm_eq_one_of_not_module_finite`, `norm_self`	7
Total	8

Algebra

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	112 math math: `norm_algebraMap_of_basis`, `Ideal.absNorm_span_insert`, `norm_eq_zero_iff_of_basis`, `NumberField.norm_norm_le_norm_mul_house_pow`, `finrank_quotient_span_eq_natDegree_norm`, `PowerBasis.norm_gen_eq_coeff_zero_minpoly`, `norm_eq_matrix_det`, `NumberField.mixedEmbedding.norm_eq_norm`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow`, `NumberField.FinitePlace.prod_eq_inv_abs_norm`, `FractionalIdeal.absNorm_eq'`, `algebraMap_intNorm`, `NumberField.Units.dirichletUnitTheorem.seq_next`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two`, `NumberField.FinitePlace.prod_eq_inv_abs_norm_int`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `discr_powerBasis_eq_norm`, `IsPrimitiveRoot.norm_eq_neg_one_pow`, `IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two`, `algebraMap_intNorm_fractionRing`, `norm_eq_prod_embeddings`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le`, `map_intNormAux`, `norm_localization`, `coe_norm_int`, `IsPrimitiveRoot.sub_one_norm_isPrimePow`, `IntermediateField.AdjoinSimple.norm_gen_eq_one`, `norm_eq_of_equiv_equiv`, `NumberField.Units.norm`, `IsPrimitiveRoot.norm_eq_one`, `norm_eq_iff`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two`, `IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two'`, `FiniteField.norm_surjective`, `norm_self`, `WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis`, `norm_inv`, `FiniteField.algebraMap_norm_eq_pow`, `WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis`, `FiniteField.algebraMap_norm_eq_prod_pow`, `groupCohomology.norm_ofAlgebraAutOnUnits_eq`, `norm_complex_eq`, `IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero`, `IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two`, `NumberField.Units.dirichletUnitTheorem.seq_norm_le`, `norm_eq_norm_adjoin`, `IsPrimitiveRoot.norm_toInteger_sub_one_eq_one`, `IntermediateField.LinearDisjoint.norm_algebraMap`, `FractionalIdeal.absNorm_eq`, `IsPrimitiveRoot.norm_sub_one_of_prime_ne_two'`, `FractionalIdeal.absNorm_span_singleton`, `IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two`, `norm_eq_prod_automorphisms`, `IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic`, `IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le`, `IsPrimitiveRoot.norm_sub_one_of_prime_ne_two`, `LinearMap.det_restrictScalars`, `IsPrimitiveRoot.norm_eq_one_of_linearly_ordered`, `ClassGroup.norm_lt`, `RingOfIntegers.coe_norm`, `intNorm_eq_norm`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two`, `Ideal.norm_mem_spanNorm`, `IsPrimitiveRoot.norm_pow_sub_one_two`, `norm_complex_apply`, `associated_norm_prod_smith`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two`, `norm_eq_one_of_not_exists_basis`, `norm_eq_of_algEquiv`, `IsPrimitiveRoot.card_quotient_toInteger_sub_one`, `IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots`, `NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr`, `norm_one_add_smul`, `norm_apply`, `WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two`, `FiniteField.unitsMap_norm_surjective`, `norm_eq_prod_roots`, `norm_zero`, `norm_eq_one_of_not_module_finite`, `norm_norm`, `FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm`, `IsCyclotomicExtension.norm_zeta_eq_one`, `IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one`, `IsCyclotomicExtension.norm_zeta_pow_sub_one_two`, `RingOfIntegers.algebraMap_norm_algebraMap`, `PowerBasis.norm_gen_eq_prod_roots`, `Subalgebra.LinearDisjoint.norm_algebraMap`, `NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr`, `norm_algebraMap`, `NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply`, `Ideal.norm_mem_relNorm`, `norm_eq_zero_iff`, `NumberField.InfinitePlace.prod_eq_abs_norm`, `norm_eq_of_ringEquiv`, `Ideal.absNorm_span_singleton`, `ClassGroup.norm_le`, `RingOfIntegers.coe_algebraMap_norm`, `IsPrimitiveRoot.norm_of_cyclotomic_irreducible`, `isIntegral_norm`, `norm_eq_prod_embeddings_gen`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two'`, `FiniteField.algebraMap_norm_eq_pow_sum`, `IsPrimitiveRoot.norm_sub_one_two`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two`, `ClassGroup.exists_mem_finset_approx'`, `ClassGroup.exists_mem_finsetApprox`, `IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two`, `prod_galRestrict_eq_norm`, `Ideal.absNorm_dvd_norm_of_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `norm` `RingHom` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toModule`	—	`norm_algebraMap_of_basis` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `EuclideanDomain.toNontrivial` `norm_eq_one_of_not_exists_basis` `finrank_eq_zero_of_not_exists_basis` `Module.Free.of_divisionRing` `pow_zero`
`norm_algebraMap_of_basis` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm` `RingHom` `RingHom.instFunLike` `algebraMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	`smulCommClass_self` `IsScalarTower.left` `norm_apply` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.det_toMatrix` `IsScalarTower.to_smulCommClass'` `lmul_algebraMap` `Matrix.ext` `toMatrix_lsmul` `Finset.prod_const` `Finset.card_univ` `Matrix.det_diagonal`
`norm_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm` `LinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `toModule` `Module.End.instSemiring` `LinearMap.det` `AlgHom` `Module.End` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul`	—	—
`norm_eq_matrix_det` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm` `Matrix.det` `AlgHom` `Matrix` `Matrix.semiring` `Matrix.instAlgebra` `id` `AlgHom.funLike` `leftMulMatrix`	—	`smulCommClass_self` `IsScalarTower.left` `norm_apply` `RingHomInvPair.ids` `Finite.of_fintype` `LinearMap.det_toMatrix` `to_smulCommClass` `toMatrix_lmul_eq`
`norm_eq_one_of_not_exists_basis` 📖	mathematical	`Module.Basis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toModule` `Ring.toSemiring`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `norm` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`smulCommClass_self` `IsScalarTower.left` `norm_apply` `LinearMap.det_def`
`norm_eq_one_of_not_module_finite` 📖	mathematical	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toModule` `Ring.toSemiring`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `norm` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`norm_eq_one_of_not_exists_basis` `Module.Finite.of_basis` `Finite.of_fintype`
`norm_self` 📖	mathematical	—	`norm` `CommRing.toRing` `id` `CommRing.toCommSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`MonoidHom.ext` `smulCommClass_self` `to_smulCommClass` `IsScalarTower.right` `LinearMap.det_ring` `mul_one`

---

← Back to Index