Theorem frobenius_inj
Modification history
2022-02-16 17:16
src/algebra/char_p/basic.lean
feat(algebra/char_p/basic): Generalize `frobenius_inj`. (#12079)
Modified frobenius_injView on Github →2021-04-06 01:49
src/algebra/char_p/basic.lean
chore(algebra/char_p/basic): uniformise notation and weaken some assumptions (#6765) …
Modified frobenius_injView on Github →2021-01-27 05:12
src/algebra/char_p/basic.lean
chore(*): Replace integral_domain assumptions with no_zero_divisors (#5877) …
Modified frobenius_injView on Github →2020-04-25 09:58
src/algebra/char_p.lean
refactor(*): use [fact p.prime] for frobenius and perfect_closure (#2518) …
Modified frobenius_injView on Github →