Def Mathlib.Tactic.Algebraize.addAlgebraInstanceFromRingHom

Modification history

2024-10-04 10:12

Mathlib/Tactic/Algebraize.lean

feat(Tactic/Algebraize): add algebraize tactic (#16217) …

Added Mathlib.Tactic.Algebraize.addAlgebraInstanceFromRingHom View on Github →