Theorem norm_sub_mul_le'

Modification history

2025-03-09 23:03
Mathlib/Analysis/Normed/Field/Basic.lean
refactor(Mathlib/Analysis/Normed): disentangle normed rings and normed fields (#22744) …
Modified norm_sub_mul_le'View on Github →
2024-09-02 07:30
Mathlib/Analysis/Normed/Field/Basic.lean
feat: `‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖` when `‖a‖ ≤ 1` (#16318) …
Added norm_sub_mul_le'View on Github →