Topological (sub)algebras over Rat

Results

This is just a minimal stub for now!

instance DivisionRing.continuousConstSMul_rat {A : Type u_1} [DivisionRing A] [TopologicalSpace A] [ContinuousMul A] [CharZero A] : ContinuousConstSMul ℚ A

The action induced by DivisionRing.toRatAlgebra is continuous.

Equations

• ⋯ = ⋯