Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-14 09:48 3c771674

View on Github →

feat(linear_algebra/dual): generalize from field to ring (#7599)

Estimated changes

Modified src/linear_algebra/dual.lean

modified theorem basis.coe_to_dual_self

modified def basis.dual_basis

modified theorem basis.dual_basis_apply

modified theorem basis.dual_basis_equiv_fun

modified theorem basis.dual_basis_repr

modified theorem basis.dual_dim_eq

added def basis.eval_equiv

added theorem basis.eval_equiv_to_linear_map

added theorem basis.eval_ker

added theorem basis.eval_range

modified def basis.to_dual

modified theorem basis.to_dual_apply_left

modified theorem basis.to_dual_apply_right

modified theorem basis.to_dual_eq_equiv_fun

modified theorem basis.to_dual_eq_repr

modified def basis.to_dual_equiv

modified def basis.to_dual_flip

modified theorem basis.to_dual_flip_apply

modified theorem basis.to_dual_inj

modified theorem basis.to_dual_ker

modified theorem basis.to_dual_range

modified theorem basis.to_dual_total_left

modified theorem basis.to_dual_total_right

modified theorem basis.total_coord

modified theorem basis.total_dual_basis

modified def dual_pair.basis

modified def dual_pair.coeffs

modified theorem dual_pair.coeffs_apply

modified theorem dual_pair.coeffs_lc

modified theorem dual_pair.dual_lc

modified def dual_pair.lc

modified theorem dual_pair.lc_coeffs

modified theorem dual_pair.lc_def

modified theorem dual_pair.mem_of_mem_span

modified structure dual_pair