∫ Утверждение Mathlib

exists_one_lt_mul_of_lt'

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

URI: https://scilib.ai/kg/mathlib#exists_one_lt_mul_of_lt'

← MathLib Explorer