Def NormedDivisionRing.induced

Modification history

2024-05-07 01:05

Mathlib/Analysis/Normed/Field/Basic.lean

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

Deleted NormedDivisionRing.induced View on Github →

2023-03-13 13:27

Mathlib/Analysis/Normed/Field/Basic.lean

feat: port Analysis.Normed.Field.Basic (#2792)

Added NormedDivisionRing.induced View on Github →