Mathlib Changelog
v4
Changelog
About
Github
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 →