Skip to content

[Merged by Bors] - doc(Tactic/Ring/Basic): fix documentation for ExProd.mkRat #63040

[Merged by Bors] - doc(Tactic/Ring/Basic): fix documentation for ExProd.mkRat

[Merged by Bors] - doc(Tactic/Ring/Basic): fix documentation for ExProd.mkRat #63040

label-and-report-new-contributor

succeeded Feb 25, 2025 in 3s