Documentation Verification Report

House

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

Statistics

Metric	Count
Definitions `house`	1
Theorems `exists_conjugate_one_le_norm`, `basis_repr_norm_le_const_mul_house`, `exists_ne_zero_int_vec_house_le`, `house_add_le`, `house_eq_sup'`, `house_intCast`, `house_mul_le`, `house_nat_mul`, `house_nonneg`, `house_pow_le`, `house_prod_le`, `house_sum_le_sum_house`, `norm_embedding_le_house`, `norm_norm_le_norm_mul_house_pow`, `one_le_house_of_isIntegral`	15
Total	16

NumberField

Definitions

Name	Category	Theorems
`house` 📖	CompOp	13 math math: `norm_norm_le_norm_mul_house_pow`, `house_intCast`, `house_mul_le`, `house_sum_le_sum_house`, `house_pow_le`, `one_le_house_of_isIntegral`, `house_nonneg`, `norm_embedding_le_house`, `house_nat_mul`, `house_add_le`, `house_prod_le`, `house.basis_repr_norm_le_const_mul_house`, `house_eq_sup'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_conjugate_one_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `RingOfIntegers.val`	—	`instNonemptyInfinitePlaceOfRingHomComplex` `Embeddings.instNonemptyRingHom` `Complex.instCharZero` `Complex.isAlgClosed` `InfinitePlace.one_le_of_lt_one` `LT.lt.not_ge` `InfinitePlace.norm_embedding_eq`
`house_add_le` 📖	mathematical	—	`Real` `Real.instLE` `house` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instAdd`	—	`Complex.instCharZero` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `norm_add_le`
`house_eq_sup'` 📖	mathematical	—	`house` `NNReal.toReal` `Finset.sup'` `NNReal` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `instSemilatticeSupNNReal` `Finset.univ` `Embeddings.instFintypeRingHom` `Complex.instField` `Complex.instCharZero` `Finset.univ_nonempty` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DFunLike.coe` `RingHom.instFunLike`	—	`Complex.instCharZero` `Finset.univ_nonempty` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `house.eq_1` `coe_nnnorm` `canonicalEmbedding.nnnorm_eq` `Finset.sup'_eq_sup`
`house_intCast` 📖	mathematical	—	`house` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup`	—	`Complex.instCharZero` `map_intCast` `RingHom.instRingHomClass` `pi_norm_const` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `Complex.norm_intCast` `Int.cast_abs` `Real.instIsStrictOrderedRing`
`house_mul_le` 📖	mathematical	—	`Real` `Real.instLE` `house` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instMul`	—	`Complex.instCharZero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `norm_mul_le`
`house_nat_mul` 📖	mathematical	—	`house` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instMul` `Real.instNatCast`	—	`Complex.instCharZero` `Finset.univ_nonempty` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `house_eq_sup'` `Finset.sup'_eq_sup` `NNReal.coe_natCast` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_natCast` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `Complex.nnnorm_natCast` `NNReal.mul_finset_sup`
`house_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `house`	—	`norm_nonneg` `Complex.instCharZero`
`house_pow_le` 📖	mathematical	—	`Real` `Real.instLE` `house` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instMonoid`	—	`Complex.instCharZero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `norm_pow_le` `Pi.normOneClass` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `NormedDivisionRing.to_normOneClass`
`house_prod_le` 📖	mathematical	—	`Real` `Real.instLE` `house` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instCommMonoid`	—	`Complex.instCharZero` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finset.prod_congr` `Finset.norm_prod_le` `Pi.normOneClass` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `NormedDivisionRing.to_normOneClass`
`house_sum_le_sum_house` 📖	mathematical	—	`Real` `Real.instLE` `house` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instAddCommMonoid`	—	`Complex.instCharZero` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `norm_sum_le_of_le` `le_refl`
`norm_embedding_le_house` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `house`	—	`Complex.instCharZero` `Finset.univ_nonempty` `Embeddings.instNonemptyRingHom` `Complex.isAlgClosed` `house_eq_sup'` `Finset.le_sup'` `Finset.mem_univ`
`norm_norm_le_norm_mul_house_pow` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `Rat.instNormedField` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rat.commRing` `MonoidHom.instFunLike` `Algebra.norm` `DivisionRing.toRatAlgebra` `to_charZero` `Real.instMul` `Complex` `Complex.instNorm` `RingHom` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `Monoid.toNatPow` `Real.instMonoid` `house` `Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring`	—	`to_charZero` `Complex.instCharZero` `instIsDomain` `to_finiteDimensional` `Algebra.norm_eq_prod_embeddings` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `PerfectField.ofCharZero` `Rat.instCharZero` `Complex.isAlgClosed` `Rat.norm_cast_real` `Real.norm_eq_abs` `eq_ratCast` `RingHom.instRingHomClass` `Complex.norm_ratCast` `Finset.mul_prod_erase` `Finset.mem_univ` `Complex.norm_mul` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Finset.norm_prod_le` `NormedDivisionRing.to_normOneClass` `norm_nonneg` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `norm_embedding_le_house` `Finset.prod_const` `Finset.card_erase_of_mem` `AlgHom.card`
`one_le_house_of_isIntegral` 📖	mathematical	`IsIntegral` `Int.instCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toIntAlgebra`	`Real` `Real.instLE` `Real.instOne` `house`	—	`exists_conjugate_one_le_norm` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `LE.le.trans` `norm_embedding_le_house`

NumberField.house

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_repr_norm_le_const_mul_house` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instRatCast` `DFunLike.coe` `Finsupp` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Rat.semiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Rat.commSemiring` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Module.Basis.reindex` `Module.Free.ChooseBasisIndex` `NumberField.RingOfIntegers` `Int.instSemiring` `NumberField.RingOfIntegers.instCommRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `NumberField.RingOfIntegers.instFreeInt` `NumberField.integralBasis` `Equiv.symm` `NumberField.equivReindex` `NumberField.RingOfIntegers.val` `Real.instMul` `NumberField.house` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Algebra.id` `Semifield.toCommSemiring`	—	`RingHomInvPair.ids` `NumberField.to_charZero` `NumberField.RingOfIntegers.instFreeInt` `Complex.instCharZero` `NumberField.inverse_basisMatrix_mulVec_eq_repr` `norm_sum_le_of_le` `Eq.le` `norm_mul` `NormedDivisionRing.toNormMulClass` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Matrix.norm_entry_le_entrywise_sup_norm` `norm_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `norm_le_pi_norm` `Finset.sum_const` `NumberField.Embeddings.card` `Complex.isAlgClosed` `nsmul_eq_mul` `mul_assoc`
`exists_ne_zero_int_vec_house_le` 📖	mathematical	`Fintype.card` `Real` `Real.instLE` `NumberField.house` `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`	`Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Subalgebra` `Int.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Ring.toIntAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Real.instMul` `Real.instPow` `Real.instNatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub`	—	`NumberField.to_charZero` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `Module.finrank_pos` `commRing_strongRankCondition` `Rat.nontrivial` `NumberField.to_finiteDimensional` `Rat.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `mul_pos_iff` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Complex.instCharZero` `Fintype.card_prod` `NumberField.Embeddings.card` `Complex.isAlgClosed` `Int.Matrix.exists_ne_zero_int_vec_norm_le'` `Fintype.card_pos_iff` `LT.lt.trans` `le_trans` `NumberField.house_nonneg` `mul_div_mul_right` `Nat.cast_zero` `RCLike.charZero_rclike` `LT.lt.ne'` `sub_mul` `Nat.cast_mul`

---

← Back to Index