Commit 2025-04-06 22:31 dbd5552b

View on Github →

feat(EGauge): add egauge_pi and egauge_prod (#23206) Also change recently introduced smul_set*pi* to use unapplied smul in the rhs.

Estimated changes

modified theorem Set.smul_set_univ_pi
added theorem Set.smul_set_pi₀'
added theorem Set.MapsTo.egauge_le
added theorem egauge_pi'
added theorem egauge_pi
added theorem egauge_prod_mk
added theorem egauge_univ_pi
added theorem le_egauge_pi
added theorem le_egauge_prod
added theorem mem_smul_of_egauge_lt
added theorem exists_enorm_lt'