Def Module.RestrictScalars.normedAlgebraOrig

Modification history

2024-02-14 14:03
Mathlib/Analysis/NormedSpace/Basic.lean
feat: `NormedAlgebra.complexToReal` and other `RestrictScalars` instances (#10374) …
Added Module.RestrictScalars.normedAlgebraOrigView on Github →