Commit 2022-01-16 13:03 d60541cc

View on Github →

feat(analysis/seminorm): Add has_add and has_scalar nnreal (#11414) Add instances of has_add and has_scalar nnreal type classes for seminorm.

Estimated changes

Modified src/analysis/seminorm.lean

added theorem seminorm.add_apply

added theorem seminorm.coe_add

added def seminorm.coe_fn_add_monoid_hom

added theorem seminorm.coe_fn_add_monoid_hom_injective

added theorem seminorm.coe_smul

added theorem seminorm.smul_apply