Theorem NonarchimedeanRing.mul_subset

Modification history

2023-03-17 16:27
Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
feat: port Topology.Algebra.Nonarchimedean.Basic (#2958)
Added NonarchimedeanRing.mul_subsetView on Github →