Theorem Mathlib.Tactic.Algebra.smul_one_eq_smul_one'

Modification history

2026-04-16 17:52
Mathlib/Tactic/Algebra/Lemmas.lean
feat(Tactic): `algebra` tactic. (#31508) …
Added Mathlib.Tactic.Algebra.smul_one_eq_smul_one'View on Github →