Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
sylow.mk_vector_prod_eq_one_injective
Modification history
2021-09-06 12:25
src/group_theory/sylow.lean
refactor(group_theory/*): Move Cauchy's theorem (#8916) …
Deleted
sylow.mk_vector_prod_eq_one_injective
View on Github →
2020-06-18 22:26
src/group_theory/sylow.lean
chore(*): regularize naming using injective (#3071) …
Added
sylow.mk_vector_prod_eq_one_injective
View on Github →