Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-04-26 15:11
3877d4f0
View on Github →
chore: remove a subsingleton instance which leads to unreasonable instance search paths (
#12445
)
Estimated changes
Modified
Mathlib/Algebra/CharP/Basic.lean
added
theorem
CharP.CharOne.subsingleton
modified
theorem
CharP.false_of_nontrivial_of_char_one
Modified
Mathlib/Data/ZMod/Basic.lean