Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 21:04 274b5309

View on Github →

feat(data/equiv/basic): add add_equiv.to_int_linear_equiv (#11456) as written by @adamtopaz on zulip

Estimated changes

Modified src/data/equiv/module.lean

added theorem add_equiv.coe_to_int_linear_equiv

added theorem add_equiv.coe_to_linear_equiv

added theorem add_equiv.coe_to_linear_equiv_symm

added theorem add_equiv.coe_to_nat_linear_equiv

added def add_equiv.to_int_linear_equiv

added theorem add_equiv.to_int_linear_equiv_refl

added theorem add_equiv.to_int_linear_equiv_symm

added theorem add_equiv.to_int_linear_equiv_to_add_equiv

added theorem add_equiv.to_int_linear_equiv_trans

added def add_equiv.to_linear_equiv

added def add_equiv.to_nat_linear_equiv

added theorem add_equiv.to_nat_linear_equiv_refl

added theorem add_equiv.to_nat_linear_equiv_symm

added theorem add_equiv.to_nat_linear_equiv_to_add_equiv

added theorem add_equiv.to_nat_linear_equiv_trans

added theorem linear_equiv.to_add_equiv_to_int_linear_equiv

added theorem linear_equiv.to_add_equiv_to_nat_linear_equiv

Modified src/linear_algebra/basic.lean

deleted theorem add_equiv.coe_to_linear_equiv

deleted theorem add_equiv.coe_to_linear_equiv_symm

deleted def add_equiv.to_linear_equiv