Commit 2024-10-04 04:46 149d450d

View on Github →

feat: Order properties of Pi.single (#17281) From LeanCamCombi

Estimated changes

added theorem Pi.mulSingle_le_one
added theorem Pi.one_le_mulSingle