Theorem mul_left_iterate_apply_self

Modification history

2026-09-11 08:52

Mathlib/Algebra/Group/Basic.lean

refactor: allow non-unital normed rings in `HasSummableGeomSeries` (#43141) …

Added mul_left_iterate_apply_self View on Github →