Mathlib Changelog
v3
Changelog
About
Github
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