Skip to content

[Merged by Bors] - doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations #5278

[Merged by Bors] - doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations

[Merged by Bors] - doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations #5278

Annotations

1 warning

Fix style issues from lint

succeeded Jan 26, 2025 in 4s