Theorem RCLike.re_extendTo𝕜'ₗ

Modification history

2025-08-22 20:24

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

refactor: Use `StrongDual` (#28726) …

Modified RCLike.re_extendTo𝕜'ₗ View on Github →

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 →

2024-08-09 00:58

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

chore: backports for leanprover/lean4#4814 (part 33) (#15605)

Modified RCLike.re_extendTo𝕜'ₗ View on Github →

2024-08-02 21:35

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

feat: `RCLike` versions of Hahn-Banach separation theorems (#15416) …

Added RCLike.re_extendTo𝕜'ₗ View on Github →