Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-22 12:22 93b17864

View on Github →

feat(archive): add proof of sensitivity conjecture (#1553)

  • feat(*): various lemmas from the sensitivity project
  • fix proof broken by nonterminal simp
  • Update src/linear_algebra/dual.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • lint dual.lean
  • remove decidable_mem_of_fintype instance this leads to loops with subtype.fintype under the right decidable_eq assumptions
  • dual_lc is invalid simp lemma
  • fix namespace
  • add extra lemma
  • feat(archive): add proof of sensitivity conjecture
  • suggestions from Johan
  • undo removed whitespace
  • update header

Estimated changes

added theorem Q.adj_iff_proj_adj
added theorem Q.adj_iff_proj_eq
added theorem Q.adjacent.symm
added def Q.adjacent
added theorem Q.card
added theorem Q.not_adjacent_zero
added theorem Q.succ_n_eq
added def V.has_add
added def V.has_scalar
added def V.module
added def V
added theorem dim_V
added def dual_pair_e_ε
added theorem duality
added theorem e_zero_apply
added theorem epsilon_total
added theorem exists_eigenvalue
added theorem f_image_g
added theorem f_matrix
added theorem f_squared
added theorem f_succ_apply
added theorem f_zero
added theorem findim_V
added theorem g_apply
added theorem g_injective
added theorem huang_degree_theorem
added def π