Commit 2025-07-15 08:11 de0a2931
View on Github →doc(Algebra/Homology/Homotopy): add field docstrings to HomotopyEquiv (#27048)
Split of https://github.com/leanprover-community/mathlib4/pull/25917. Adds docstrings to fields of a structure that did not have them. Note: this documentation was written by asking Cursor (Claude 3.5 sonnet) to write the docstrings.