Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-20 21:37 0dbe3a94

View on Github →

feat(algebra,equiv,logic): add various lemmas (#1342)

add various lemmas
add simp lemma
fix simp
rename to subtype_sigma_equiv

Estimated changes

Modified src/algebra/order_functions.lean

added theorem fn_min_add_fn_max

added theorem fn_min_mul_fn_max

added theorem min_add_max

added theorem min_mul_max

Modified src/algebra/ordered_ring.lean

added theorem mul_self_add_mul_self_eq_zero

Modified src/algebra/ring.lean

added theorem Vieta_formula_quadratic

added theorem mul_self_eq_zero

added theorem zero_eq_mul_self

Modified src/data/equiv/basic.lean

added def equiv.subtype_sigma_equiv

Modified src/data/list/basic.lean

modified theorem list.tfae_singleton

Modified src/logic/basic.lean

added theorem eq.congr_left

added theorem eq.congr_right

added theorem eq_iff_iff