Commit 2024-12-05 01:28 80e107a9

View on Github →

chore: add more gcongr attributes (#17610) This PR tags (analogues of) lemmas tagged with mono also with gcongr.

Estimated changes

modified theorem AddSubmonoid.mul_le_mul
added theorem Real.arctan_le_arctan
added theorem Real.arctan_lt_arctan
added theorem Basis.flag_le_flag
added theorem Basis.flag_lt_flag