Theorems · Theorem · number theory
Height.mulHeight_sumElim_zero_eq
∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
[Finite ι'] (x : ι → K), Height.mulHeight (Sum.elim x 0) = Height.mulHeight x- Defined in
- Mathlib.NumberTheory.Height.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Set.Elemproof · cited by 7,166
- Finitestatement and proof · cited by 3,029
- Multisetproof · cited by 2,627
- iSupproof · cited by 2,415
- CommMonoidproof · cited by 2,264
- le_antisymmproof · cited by 2,068
- le_rflproof · cited by 1,558
- eq_or_neproof · cited by 1,117
- Multiset.mapproof · cited by 876
Cited by3
Results whose statement or proof uses this declaration.
- Height.mulHeight_cons_zeroproof · cited by 2
- Height.mulHeight_eq_mulHeight_restrict_supportproof · cited by 1
- Height.logHeight_sumElim_zero_eqproof · cited by 0