Mathlib Changelog
v4
Changelog
About
Github
Theorem
OreLocalization.add''_char
Modification history
2026-03-10 12:49
Mathlib/RingTheory/OreLocalization/Basic.lean
chore: remove unnecessary private and backward.privateInPublic (#36430) …
Added
OreLocalization.add''_char
View on Github →