Theorems · Theorem · real analysis
ENNReal.mul_left_inj
∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)- Defined in
- Mathlib.Data.ENNReal.Operations
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- mul_commproof · cited by 2,262
- ENNReal.mul_right_injproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- Dilation.ratio_uniqueproof · cited by 3
- Dilation.ratio_comp'proof · cited by 3
- AddMonoidHom.measurePreservingproof · cited by 2
- MonoidHom.measurePreservingproof · cited by 2
- ProbabilityTheory.Kernel.measure_eq_zero_or_one_or_top_of_indepSet_selfproof · cited by 2
- ENNReal.mul_eq_rightproof · cited by 0