Theorem is_primitive_root.of_map_of_injective
Modification history
2022-08-11 21:15
src/ring_theory/roots_of_unity.lean
feat(ring_theory/roots_of_unity): generalisation linter (#16014) …
Modified is_primitive_root.of_map_of_injectiveView on Github →2022-01-31 11:21
src/ring_theory/roots_of_unity.lean
feat(ring_theory/roots_of_unity): `fun_like` support (#11735) …
Modified is_primitive_root.of_map_of_injectiveView on Github →