Theorem NonarchAddGroupSeminorm.zero_apply

Modification history

2026-07-17 23:35
Mathlib/Analysis/Normed/Group/Seminorm.lean
feat(Analysis): use `IsApply` for `GroupSeminorm` (#41560) …
Deleted NonarchAddGroupSeminorm.zero_applyView on Github →
2023-03-09 00:44
Mathlib/Analysis/Normed/Group/Seminorm.lean
feat: port Analysis.Normed.Group.Seminorm (#2400) …
Added NonarchAddGroupSeminorm.zero_applyView on Github →