Commit 2024-07-18 07:43 21afd967

View on Github →

feat: normed structure instances for SetLike subobjects (#14545)

Estimated changes

Modified Mathlib/Analysis/Normed/Field/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem SubgroupClass.coe_norm

Modified Mathlib/Analysis/Normed/Group/Submodule.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean