Commit 2023-02-03 23:53 a234da04

View on Github →

chore: fix naming in ConstMulAction.lean (#2047) This corrects some Smuls introduced in #2012 to SMul.

Estimated changes

modified theorem IsCompact.smul
modified theorem isOpenMap_quotient_mk'_mul