Commit 2024-09-14 05:03 9785e5e9
View on Github →chore: Minor hypothesis changes, and a small lemma allowing ContinuousSMul to descend an IsScalarTower (#16777)
The main contribution here is IsScalarTower.continuousSMul, which is then used in the Separation.lean file to improve the geometric Hahn Banach proofs for RCLike fields.