Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-12 18:27 1b3556cc

View on Github →

chore(linear_algebra): rename dual_pair (#16482) This only renames dual_pair to module.dual_bases, avoiding to put a very generic name into the root name space. This dual_pair was used only in the archive, I introduced it a very long time ago to streamline the proof of the sensitivity conjecture.

Estimated changes

Modified archive/sensitivity.lean

added def dual_bases_e_ε

deleted def dual_pair_e_ε

Modified src/linear_algebra/dual.lean

deleted def dual_pair.basis

deleted theorem dual_pair.coe_basis

deleted theorem dual_pair.coe_dual_basis

deleted def dual_pair.coeffs

deleted theorem dual_pair.coeffs_apply

deleted theorem dual_pair.coeffs_lc

deleted theorem dual_pair.dual_lc

deleted def dual_pair.lc

deleted theorem dual_pair.lc_coeffs

deleted theorem dual_pair.lc_def

deleted theorem dual_pair.mem_of_mem_span

deleted structure dual_pair

added def module.dual_bases.basis

added theorem module.dual_bases.coe_basis

added theorem module.dual_bases.coe_dual_basis

added def module.dual_bases.coeffs

added theorem module.dual_bases.coeffs_apply

added theorem module.dual_bases.coeffs_lc

added theorem module.dual_bases.dual_lc

added def module.dual_bases.lc

added theorem module.dual_bases.lc_coeffs

added theorem module.dual_bases.lc_def

added theorem module.dual_bases.mem_of_mem_span

added structure module.dual_bases