Commit 2024-07-16 22:33 6f640f86

View on Github →

feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras (#14611) This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean

added theorem Subalgebra.comm_trans_lTensorBot

added theorem Subalgebra.comm_trans_rTensorBot

added theorem Subalgebra.finrank_sup_le_of_free

added def Subalgebra.lTensorBot

added theorem Subalgebra.lTensorBot_one_tmul

added theorem Subalgebra.lTensorBot_symm_apply

added theorem Subalgebra.lTensorBot_tmul

added def Subalgebra.mulMap'

added theorem Subalgebra.mulMap'_surjective

added def Subalgebra.mulMap

added theorem Subalgebra.mulMap_bot_left_eq

added theorem Subalgebra.mulMap_bot_right_eq

added theorem Subalgebra.mulMap_comm

added theorem Subalgebra.mulMap_range

added theorem Subalgebra.mulMap_tmul

added theorem Subalgebra.mulMap_toLinearMap

added def Subalgebra.rTensorBot

added theorem Subalgebra.rTensorBot_symm_apply

added theorem Subalgebra.rTensorBot_tmul

added theorem Subalgebra.rTensorBot_tmul_one

added theorem Subalgebra.rank_sup_le_of_free

added theorem Subalgebra.val_mulMap'_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Submodule.lean