feat: add ContinuousSMul instances for ℚ≥0
#239664
Annotations
2 errors
|
lint mathlib
Process completed with exit code 1.
|
|
lint mathlib:
Mathlib/Topology/Instances/Rat.lean#L131
@NNRat.instContinuousSMulOfRingOfRat argument 2 inst✝³ : Ring
|
Loading