Commit 2021-08-25 10:57 8d645036

View on Github →

port init/algebra/functions.lean (#45)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/Algebra/Functions.lean

added theorem eq_max

added theorem eq_min

added theorem le_max_left

added theorem le_max_right

added theorem le_min

added theorem lt_min

added theorem max_assoc

added theorem max_comm

added theorem max_eq_left

added theorem max_eq_left_of_lt

added theorem max_eq_right

added theorem max_eq_right_of_lt

added theorem max_le

added theorem max_left_comm

added theorem max_lt

added theorem max_self

added theorem min_assoc

added theorem min_comm

added theorem min_eq_left

added theorem min_eq_left_of_lt

added theorem min_eq_right

added theorem min_eq_right_of_lt

added theorem min_le_left

added theorem min_le_right

added theorem min_left_comm

added theorem min_self

Modified Mathlib/Init/Logic.lean

added def associative

added def commutative

added def left_cancelative

added theorem left_comm

added def left_commutative

added def left_distributive

added def left_identity

added def right_cancelative

added theorem right_comm

added def right_commutative

added def right_distributive

added def right_identity

added def right_inverse