Commit 2023-06-18 07:26 6f65fafe

View on Github →

chore: fix a typo (#5202) Introduced while making it multiplicative in leanprover-community/mathlib#13359

Estimated changes