ProductFormula

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

Statistics

Metric	Count
Definitions	0
Theorems prod_eq_inv_abs_norm, prod_eq_inv_abs_norm_int, prod_abs_eq_one	3
Total	3

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_abs_eq_one 📖	mathematical	—	Real Real.instMul Finset.prod InfinitePlace Real.instCommMonoid Finset.univ InfinitePlace.NumberField.InfinitePlace.fintype Monoid.toPow Real.instMonoid DFunLike.coe InfinitePlace.instFunLikeReal InfinitePlace.mult finprod FinitePlace FinitePlace.instFunLikeReal Real.instOne	—	to_charZero InfinitePlace.prod_eq_abs_norm Rat.cast_abs Real.instIsStrictOrderedRing FinitePlace.prod_eq_inv_abs_norm Rat.cast_inv RCLike.charZero_rclike mul_inv_cancel₀ IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Rat.isDomain instIsDomain Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors

NumberField.FinitePlace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_eq_inv_abs_norm 📖	mathematical	—	finprod Real NumberField.FinitePlace Real.instCommMonoid DFunLike.coe instFunLikeReal Real.instRatCast abs Rat.instLattice Rat.addGroup 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 NumberField.to_charZero	—	NumberField.to_charZero IsFractionRing.div_surjective NumberField.RingOfIntegers.instIsFractionRing map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_div map_div₀ instMonoidWithZeroHomClassReal Rat.cast_inv RCLike.charZero_rclike Rat.cast_abs Real.instIsStrictOrderedRing finprod_div_distrib hasFiniteMulSupport_int nonZeroDivisors.ne_zero prod_eq_inv_abs_norm_int inv_eq_iff_eq_inv inv_inv_div_inv abs_div Int.instIsDomain NumberField.RingOfIntegers.instFreeInt AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg NumberField.RingOfIntegers.instFG eq_div_of_mul_eq Rat.cast_intCast Algebra.coe_norm_int map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass div_mul_cancel₀ NumberField.RingOfIntegers.coe_ne_zero_iff
prod_eq_inv_abs_norm_int 📖	mathematical	—	finprod Real NumberField.FinitePlace Real.instCommMonoid DFunLike.coe instFunLikeReal NumberField.RingOfIntegers.val Real.instInv abs Real.lattice Real.instAddGroup Real.instIntCast MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing NumberField.instCommRingRingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra	—	NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg NumberField.RingOfIntegers.instFG NumberField.RingOfIntegers.instFreeInt Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup finprod_comp_equiv inv_eq_of_mul_eq_one_left Nat.cast_one Real.instIsStrictOrderedRing Int.abs_eq_natAbs Ideal.absNorm_span_singleton Ideal.finprod_heightOneSpectrum_factorization Int.cast_natCast IsScalarTower.right Ideal.finite_factors Set.Finite.subset Ideal.uniqueFactorizationMonoid Associates.count_ne_zero_iff_dvd IsDedekindDomain.HeightOneSpectrum.irreducible map_pow MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Nat.cast_pow pow_zero MonoidHom.map_finprod_of_preimage_one RCLike.charZero_rclike Ideal.one_eq_top finprod_mul_distrib finprod_eq_one_of_forall_eq_one NumberField.HeightOneSpectrum.embedding_mul_absNorm

---

← Back to Index