Theorems · Theorem · field theory
enorm_inv
∀ {α : Type u_2} [inst : NormedDivisionRing α] {a : α}, a ≠ 0 → ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 129 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- ENNReal.ofNNRealproof · cited by 1,279
- NNNorm.nnnormproof · cited by 952
- ENorm.enormstatement · cited by 715
- NormedDivisionRingstatement and proof · cited by 360
- ENNReal.coe_invproof · cited by 27
- nnnorm_invproof · cited by 14
Cited by7
Results whose statement or proof uses this declaration.
- MeasureTheory.eLpNorm_const_smulproof · cited by 4
- Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 3
- MeasureTheory.uniformIntegrable_averageproof · cited by 2
- egauge_smul_leftproof · cited by 1
- egauge_smul_rightproof · cited by 1
- MeasureTheory.eLpNorm'_const_smulproof · cited by 1
- MeasureTheory.Measure.variation_withDensityᵥproof · cited by 0