Commit 2026-07-09 05:55 ae861491

View on Github →

feat(Analysis): use Is*Apply for Seminorm (#40880)

Estimated changes

Modified Counterexamples/SeminormLatticeNotDistrib.lean

Modified Mathlib/Analysis/Seminorm.lean

deleted theorem Seminorm.add_apply

deleted def Seminorm.coeFnAddMonoidHom

deleted theorem Seminorm.coeFnAddMonoidHom_injective

deleted theorem Seminorm.coe_add

deleted theorem Seminorm.coe_smul

deleted theorem Seminorm.coe_zero

deleted theorem Seminorm.smul_apply

deleted theorem Seminorm.zero_apply