Commit 2026-01-13 09:55 b2f24e70

chore(Algebra): deduplicate IsReduced lemmas (#33775) Replace the less general versions (assuming NoZeroDivisors) under the root namespace by more general versions assuming IsReduced, and deprecate the versions under IsReduced namespace.