Commit 2023-04-04 13:30 56c1ca98

View on Github →

feat: port LinearAlgebra.Isomorphisms (#2364) This is currently stuck on an issue described in this Zulip thread.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Isomorphisms.lean

added theorem LinearMap.asFun_coe

added theorem LinearMap.coe_quotientInfToSupQuotient

added theorem LinearMap.comap_leq_ker_subToSupQuotient

added theorem LinearMap.quotKerEquivRange_apply_mk

added theorem LinearMap.quotKerEquivRange_symm_apply_image

added theorem LinearMap.quotientInfEquivSupQuotient_apply_mk

added theorem LinearMap.quotientInfEquivSupQuotient_injective

added theorem LinearMap.quotientInfEquivSupQuotient_surjective

added theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff

added theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_left

added theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_right

added def LinearMap.quotientInfToSupQuotient

added def LinearMap.subToSupQuotient

added theorem Submodule.card_quotient_mul_card_quotient

added def Submodule.quotientQuotientEquivQuotient

added def Submodule.quotientQuotientEquivQuotientAux

added theorem Submodule.quotientQuotientEquivQuotientAux_mk

added theorem Submodule.quotientQuotientEquivQuotientAux_mk_mk