Commit 2023-06-21 01:19 16962a2c

View on Github →

feat: drop unneeded assumptions (#5296) Drop unneeded assumptions in gauge_lt_one_of_mem_of_open and gauge_lt_of_mem_smul

Estimated changes

modified theorem gauge_lt_of_mem_smul
modified theorem gauge_lt_one_of_mem_of_open