Theorem AlgHom.bijective

Modification history

2023-07-27 01:08

Mathlib/RingTheory/Algebraic.lean

chore(FieldTheory/Adjoin): remove unnecessary assumptions in `minpolynatDegree_le` and `minpoly.degree_le` (#6152) …

Modified AlgHom.bijective View on Github →

2023-05-22 18:54

Mathlib/RingTheory/Algebraic.lean

feat: port RingTheory.Algebraic (#4217)

Added AlgHom.bijective View on Github →