mathlib3
02c4026c
- fix(algebra/group_power/lemmas): fix the name of sub_one_zsmul (#18109)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
fix(algebra/group_power/lemmas): fix the name of sub_one_zsmul (#18109) The old name was `zsmul_sub_one`, which didn't makes sense for the lemma statement ```lean ∀ {G : Type u_2} [_inst_1 : add_group G] (a : G) (n : ℤ), (n - 1) • a = n • a + -a ```
Author
eric-wieser
Parents
51a845f0
Loading