Def Mathlib.Tactic.Algebraize.addIsScalarTowerInstanceFromRingHomComp

Modification history

2024-10-04 10:12
Mathlib/Tactic/Algebraize.lean
feat(Tactic/Algebraize): add algebraize tactic (#16217) …
Added Mathlib.Tactic.Algebraize.addIsScalarTowerInstanceFromRingHomCompView on Github →