Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 12:09 6309c816

View on Github →

chore(ring_theory/adjoin) elab_as_eliminator attribute (#9168)

Estimated changes

modified theorem algebra.adjoin_induction