Commit 2021-08-17 10:02 51e23146

View on Github →

port remaining items from 'section propositional' in logic/basic (#36)

Estimated changes

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Init/Logic.lean

added theorem And.left_comm

added theorem Bool.ff_ne_tt

deleted theorem and_left_comm

deleted theorem bool.ff_ne_tt

Modified Mathlib/Logic/Basic.lean

added theorem And.congr_left_iff

added theorem And.congr_right_iff

added theorem And.imp_left

added theorem And.imp_right

added theorem And.right_comm

added theorem And.rotate

added theorem Decidable.iff_iff_not_or_and_or_not

added theorem Decidable.not_imp_self

added theorem Not.decidable_imp_symm

added theorem Not.imp_symm

added theorem Or.elim3

added theorem and_congr_left'

added theorem and_congr_left

added theorem and_congr_right'

added theorem and_iff_left_iff_imp

added theorem and_iff_left_of_imp

added theorem and_iff_not_or_not

added theorem and_iff_right_iff_imp

added theorem and_iff_right_of_imp

added theorem and_not_self_iff

added theorem and_or_distrib_left

added theorem and_or_distrib_right

added theorem and_self_left

added theorem and_self_right

added theorem by_contra

added def decidable_of_bool

added def decidable_of_iff'

modified def decidable_of_iff

added theorem iff_and_self

added theorem iff_false_left

added theorem iff_false_right

added theorem iff_iff_and_or_not_and_not

added theorem iff_iff_not_or_and_or_not

added theorem iff_mpr_iff_true_intro

added theorem iff_not_comm

added theorem iff_of_false

added theorem iff_of_true

added theorem iff_self_and

added theorem iff_true_left

added theorem iff_true_right

added theorem imp.swap

added theorem imp_iff_not_or

added theorem imp_imp_imp

added theorem imp_not_comm

added theorem imp_not_self

added theorem imp_or_distrib'

added theorem imp_or_distrib

added theorem not_and'

added theorem not_and_distrib

added theorem not_and_not_right

added theorem not_and_of_not_left

added theorem not_and_of_not_or_not

added theorem not_and_of_not_right

added theorem not_and_self_iff

added theorem not_iff

added theorem not_iff_comm

added theorem not_iff_not

added theorem not_imp

added theorem not_imp_comm

added theorem not_imp_not

added theorem not_imp_of_and_not

added theorem not_imp_self

added theorem not_not

added theorem not_or_distrib

added theorem not_or_of_imp

added theorem of_not_imp

added theorem of_not_not

deleted theorem or.elim3

added theorem or_and_distrib_left

added theorem or_and_distrib_right

added theorem or_iff_left_iff_imp

added theorem or_iff_not_and_not

added theorem or_iff_not_imp_left

added theorem or_iff_not_imp_right

added theorem or_iff_right_iff_imp

added theorem or_self_left

added theorem or_self_right

added theorem peirce'

added theorem peirce

added theorem xor_comm

added theorem xor_false

added theorem xor_self

added theorem xor_true