Commit 2025-03-31 10:57 8c10b57e

View on Github →

feat(Data/ENat): multiplication and Inf/Sup lemmas (#23454) We add some lemmas for multiplication and suprema/infima for ENat, including a handful that were stated as proof_wanted.

Estimated changes

added theorem ENat.mul_top'
added theorem ENat.self_le_mul_left
added theorem ENat.self_le_mul_right
added theorem ENat.top_mul'
added theorem ENat.exists_eq_iInf
added theorem ENat.iInf_mul'
added theorem ENat.iInf_mul
added theorem ENat.iInf_mul_of_ne
added theorem ENat.iSup_mul
added theorem ENat.mul_iInf'
added theorem ENat.mul_iInf
added theorem ENat.mul_iInf_of_ne
added theorem ENat.mul_iSup
added theorem ENat.mul_sSup
added theorem ENat.sSup_mul