Theorem IsPerfectClosure.equiv_comp_equiv_apply_eq_self

Modification history

2024-03-12 11:06
Mathlib/FieldTheory/IsPerfectClosure.lean
feat(FieldTheory/IsPerfectClosure): predicate `IsPerfectClosure` (#8696) …
Added IsPerfectClosure.equiv_comp_equiv_apply_eq_selfView on Github →