Commit 2026-08-10 08:17 d390e9b7

View on Github →

chore(Order/Bounds/Basic): add missing to_dual tags (#40040) This PR adds some to_dual tags that weren't added in #35208

Estimated changes

deleted theorem DirectedOn.le_of_maximal
deleted theorem maximal_iff_isGreatest
modified theorem upperBounds_prod