Structures · Algebra
Height.AdmissibleAbsValues
A type class capturing an admissible family of absolute values.
- Defined in
- Mathlib.NumberTheory.Height.Basic
- Shape
- One type argument · adds archAbsVal, nonarchAbsVal, isNonarchimedean, hasFiniteMulSupport, product_formula
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by122
- Height.mulHeight
- Height.mulHeight₁
- Height.logHeight
- Height.AdmissibleAbsValues.nonarchAbsVal
- Height.AdmissibleAbsValues.archAbsVal
- Height.logHeight₁
- Height.totalWeight
- Height.mulHeight_zero
- Height.mulHeight_eq
- Height.mulHeight_pos
- Height.mulHeightBound
- Height.one_le_mulHeight
- Height.mulHeight_eq_one_of_subsingleton
- Height.mulHeight₁_pos
- Height.mulHeight_comp_equiv
- Height.mulHeight₁_eq_mulHeight
- Height.mulHeight_smul_eq_mulHeight
- Projectivization.mulHeight
- Height.mulHeight_one
- Projectivization.logHeight
- Height.mulHeight_sumElim_zero_eq
- Height.mulHeight_pow
- Height.mulHeight_fun_mul_eq
- Height.mulHeight_cons_cons_zero
- Height.AdmissibleAbsValues.isNonarchimedean
- Height.mulHeight_eval_le
- Height.mulHeight₁_inv
- Height.mulHeight_comp_le
- Height.mulHeight₁_pow
- Height.logHeight₁_eq_log_mulHeight₁
- Height.logHeight_eq_log_mulHeight
- Height.mulHeight₁_mul_le
- Height.mulHeight_mul_le
- Height.mulHeight₁_one
- Height.AdmissibleAbsValues.hasFiniteMulSupport
- Height.mulHeight_cons_zero
- Height.one_le_mulHeight₁
- Projectivization.one_le_mulHeight
- Projectivization.mulHeight_mk
- Height.mulHeight_eval_ge
- Height.mulHeight₁_div_eq_mulHeight
- Height.mulHeight₁_neg
- Height.mulHeight₁_add_le
- Height.mulHeight_mul_mulHeight
- Height.mulHeight₁_zero
- Height.mulHeight₁_sum_le
- Height.mulHeight_linearMap_apply_le
- Height.max_mulHeightBound_zero_one_eq_one
- Height.mulHeight_swap
- Height.mulHeight_eval_ge'
Ancestors0
No ancestors.