mathlib3
62b33339 - chore(algebra/star/chsh): `repeat`ed golf (#13499)

Commit
3 years ago
chore(algebra/star/chsh): `repeat`ed golf (#13499) Instead of having a real Gröbner tactic, we can leverage a loop of `ring, simp` to reach a goal.
Author
Parents
Loading