chore(Algebra/Order/BigOperators): follow the ₀ naming convention#39692

YaelDillies wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

YaelDillies:prod_le_primeYaelDillies/mathlib4:prod_le_primeCopy head branch name to clipboard