Theorems · Theorem · field theory
norm_div
∀ {α : Type u_2} [inst : NormedDivisionRing α] (a b : α), ‖a / b‖ = ‖a‖ / ‖b‖- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 53 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedDivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- NormedDivisionRingstatement and proof · cited by 360
- map_div₀proof · cited by 98
- normHomproof · cited by 8
Cited by53
Results whose statement or proof uses this declaration.
- Asymptotics.IsLittleO.tendsto_div_nhds_zeroproof · cited by 7
- EuclideanGeometry.dist_inversion_centerproof · cited by 5
- LSeriesSummable_of_le_const_mul_rpowproof · cited by 3
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- Complex.tendsto_norm_tan_of_cos_eq_zeroproof · cited by 3
- ZLattice.exists_forall_abs_repr_le_normproof · cited by 2
- ConvexOn.lipschitzOnWith_of_abs_leproof · cited by 2
- IsUpperSet.exists_subset_ballproof · cited by 2
- IsLowerSet.exists_subset_ballproof · cited by 2
- AkraBazziRecurrence.dist_r_b'proof · cited by 2
- Complex.hasSum_taylorSeries_logproof · cited by 2