Commit 2024-09-08 02:37 2eaa4fd7

View on Github →

chore(Combinatorics/Additive): correct docstrings (#16529) Fix incorrect or misleading docstrings. Adjust to_additive setup for APFree, following the comment in #12682.

Estimated changes

Modified Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

modified theorem ThreeGPFree.eq_right

Modified Mathlib/Tactic/ToAdditive/Frontend.lean