Scalar towers one step below an intermediate field

Mathlib's IntermediateField.isScalarTower_mid supplies IsScalarTower K E L for an intermediate field E of L / K. The same statement holds one step further down: a commutative semiring k whose actions on K and on L form a scalar tower k → K → L also acts compatibly through E.

Main results

• IntermediateField.instIsScalarTower: IsScalarTower k E L for an intermediate field E of L / K and a commutative semiring k acting compatibly on K and L.

instance IntermediateField.instIsScalarTower {k : Type u_1} {K : Type u_2} {L : Type u_3} [CommSemiring k] [Field K] [Field L] [SMul k K] [Algebra k L] [Algebra K L] [IsScalarTower k K L] (E : IntermediateField K L) : IsScalarTower k (↥E) L

Mathlib's IntermediateField.isScalarTower_mid supplies IsScalarTower K E L for an intermediate field E of L / K; this is the same statement for a commutative semiring k that acts on K compatibly with its algebra structure on L, which is what an object of L defined over k needs in order to be restricted to E.