Commit 2023-12-18 01:08 bca1c69d

View on Github →

feat: define NonUnital(Semi)NormedCommRing (#8664) This adds commutative versions of the existing NonUnital(Semi)NormedRing classes. This is essential for talking about, for example, non-unital commutative C⋆-algebras.

Estimated changes

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

added def NonUnitalNormedCommRing.induced

added def NonUnitalSeminormedCommRing.induced