Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-03 11:48
59e4a793
View on Github →
feat: port Logic.Hydra (
#2290
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/Multiset/Sections.lean
Created
Mathlib/Logic/Hydra.lean
added
theorem
Acc.cutExpand
added
def
Relation.CutExpand
added
theorem
Relation.acc_of_singleton
added
theorem
Relation.cutExpand_add_left
added
theorem
Relation.cutExpand_fibration
added
theorem
Relation.cutExpand_iff
added
theorem
Relation.cutExpand_le_invImage_lex
added
theorem
Relation.cutExpand_singleton
added
theorem
Relation.cutExpand_singleton_singleton
added
theorem
Relation.not_cutExpand_zero
added
theorem
WellFounded.cutExpand