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	14 math math: norm_norm_le_norm_mul_house_pow, house_intCast, house_mul_le, house.exists_ne_zero_int_vec_house_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	—	RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring Real Real.instLE Real.instOne Norm.norm Complex.instNorm DFunLike.coe 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 NNReal.instSemilatticeSup 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.toPow 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.toPow 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.instCommRingRingOfIntegers 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	—	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.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1	Matrix.mulVec NumberField.RingOfIntegers NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real Real.instLE NumberField.house Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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