Commit 2024-11-19 10:10 487b33d7

View on Github →

chore: fix some left/right injectivity names (#19239) Follow-up Mathlib fixes from zulip discussion.

Estimated changes

Modified Mathlib/Algebra/Group/Invertible/Defs.lean

modified theorem mul_left_inj_of_invertible

modified theorem mul_right_inj_of_invertible

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Bernstein.lean