Theorem algebraMap_cobounded_le_cobounded

Modification history

2025-11-05 14:53
Mathlib/Analysis/Normed/Module/Basic.lean
feat(Analysis/Normed/Algebra/GelfandMazur): new file (#29649) …
Deleted algebraMap_cobounded_le_coboundedView on Github →
2025-06-27 05:04
Mathlib/Analysis/Normed/Module/Basic.lean
feat: behavior of unique differentiablity under field extension (#26429) …
Added algebraMap_cobounded_le_coboundedView on Github →