Commit 2024-02-12 09:20 cd4edcb7
View on Github →chore(Tactic/GCongr): move @[gcongr] tags around (#9393)
- Add
import Mathlib.Tactic.GCongr.CoretoAlgebra/Order/Ring/Lemmas. - Move most
@[gcongr]tags next to the lemmas. See Zulip thread
chore(Tactic/GCongr): move @[gcongr] tags around (#9393)
import Mathlib.Tactic.GCongr.Core
to Algebra/Order/Ring/Lemmas.@[gcongr] tags next to the lemmas.
See Zulip thread