Def NonUnitalNormedCommRing.induced

Modification history

2024-05-07 01:05

Mathlib/Analysis/Normed/Field/Basic.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted NonUnitalNormedCommRing.induced View on Github →

2023-12-18 01:08

Mathlib/Analysis/Normed/Field/Basic.lean

feat: define `NonUnital(Semi)NormedCommRing` (#8664) …

Added NonUnitalNormedCommRing.induced View on Github →