Theorem RCLike.re_extendTođť•ś'â‚—
Modification history
2024-09-14 05:03
Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
chore: Minor hypothesis changes, and a small lemma allowing `ContinuousSMul` to descend an `IsScalarTower` (#16777) …
Modified RCLike.re_extendTo𝕜'ₗView on Github →