Transvection

📁 Source: Mathlib/LinearAlgebra/Transvection.lean

Statistics

Metric	Count
Definitions dilatransvections, transvection, transvections, transvection	4
Theorems transvection, baseChange, dilatransvections_pow_mono, inv_mem_dilatransvections_iff, inv_mem_transvections_iff, mem_dilatransvections_iff_finrank, mem_dilatransvections_iff_rank, mem_transvections, mem_transvections_iff, one_mem_dilatransvections, one_mem_transvections, refl_mem_dilatransvections, refl_mem_transvections, symm_mem_dilatransvections_iff, symm_mem_transvections_iff, apply, baseChange, coe_apply, coe_toLinearMap, det_eq_one, inv_eq, inv_eq', of_left_eq_zero, of_right_eq_zero, symm_eq, symm_eq', trans_of_left_eq, trans_of_right_eq, transvections_pow_mono, transvections_subset_dilatransvections, apply, baseChange, comp_of_left_eq, comp_of_left_eq_apply, comp_of_right_eq, comp_of_right_eq_apply, det, eq_id_of_finrank_le_one, of_left_eq_zero, of_right_eq_zero	40
Total	44

IsBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
transvection 📖	mathematical	IsBaseChange	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instFunLike endHom LinearMap.transvection Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.to_smulCommClass Algebra.id Algebra.toModule IsScalarTower.right toDual	—	LinearMap.ext smulCommClass_self IsScalarTower.to_smulCommClass' Algebra.to_smulCommClass IsScalarTower.right inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass endHom_comp_apply map_add SemilinearMapClass.toAddHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass toDual_comp_apply algebraMap_smul

LinearEquiv

Definitions

Name	Category	Theorems
dilatransvections 📖	CompOp	8 math math: symm_mem_dilatransvections_iff, dilatransvections_pow_mono, mem_dilatransvections_iff_rank, transvections_subset_dilatransvections, mem_dilatransvections_iff_finrank, refl_mem_dilatransvections, one_mem_dilatransvections, inv_mem_dilatransvections_iff
transvection 📖	CompOp	15 math math: transvection.det_eq_one, mem_transvections_iff, transvection.apply, transvection.symm_eq, transvection.coe_apply, transvection.trans_of_left_eq, transvection.of_right_eq_zero, transvection.coe_toLinearMap, transvection.of_left_eq_zero, transvection.trans_of_right_eq, transvection.inv_eq', transvection.baseChange, transvection.symm_eq', transvection.inv_eq, mem_transvections
transvections 📖	CompOp	8 math math: symm_mem_transvections_iff, one_mem_transvections, refl_mem_transvections, mem_transvections_iff, transvections_subset_dilatransvections, transvections_pow_mono, inv_mem_transvections_iff, mem_transvections

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dilatransvections_pow_mono 📖	mathematical	—	Monotone Set LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.NPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid dilatransvections	—	Set.pow_right_monotone RingHomInvPair.ids one_mem_dilatransvections
inv_mem_dilatransvections_iff 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership dilatransvections InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup	—	RingHomInvPair.ids symm_mem_dilatransvections_iff
inv_mem_transvections_iff 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership transvections InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup	—	RingHomInvPair.ids symm_mem_transvections_iff
mem_dilatransvections_iff_finrank 📖	mathematical	—	LinearEquiv DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Ring.toSemiring DivisionRing.toRing Set.instMembership dilatransvections Module.finrank Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.ids LinearMap LinearMap.instSub toLinearMap LinearMap.id Submodule.addCommMonoid Submodule.module	—	RingHomInvPair.ids RingHomSurjective.ids mem_dilatransvections_iff_rank Module.finrank.eq_1 Cardinal.one_toNat Cardinal.toNat_le_iff_le_of_lt_aleph0 Module.rank_lt_aleph0 IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing LinearMap.finiteDimensional_range Cardinal.one_lt_aleph0
mem_dilatransvections_iff_rank 📖	mathematical	—	LinearEquiv DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Ring.toSemiring DivisionRing.toRing Set.instMembership dilatransvections Cardinal Cardinal.instLE Module.rank Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.ids LinearMap LinearMap.instSub toLinearMap LinearMap.id Submodule.addCommMonoid Submodule.module Cardinal.instOne	—	RingHomInvPair.ids RingHomSurjective.ids le_trans Submodule.rank_mono add_sub_cancel_left rank_span_le IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Cardinal.mk_fintype Fintype.card_unique Nat.cast_one LinearMap.ext LinearMap.mem_range_self rank_zero_iff DivisionRing.isDomain Ideal.instIsTorsionFreeSubtypeMemSubmodule instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors eq_sub_iff_add_eq zero_add LinearMap.transvection.of_right_eq_zero le_antisymm Cardinal.one_le_iff_ne_zero finrank_eq_one_iff Module.Free.of_divisionRing Module.rank_eq_one_iff_finrank_eq_one RingHomCompTriple.ids LinearMap.transvection.apply add_comm LinearMap.codRestrict_apply IsScalarTower.left Submodule.coe_smul Module.Basis.linearCombination_repr Finsupp.linearCombination_apply Finsupp.sum_eq_single IsDomain.toIsCancelMulZero instIsEmptyFalse zero_smul
mem_transvections 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearEquiv RingHomInvPair.ids Set Set.instMembership transvections transvection	—	—
mem_transvections_iff 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership transvections transvection	—	RingHomInvPair.ids
one_mem_dilatransvections 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership dilatransvections InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup	—	refl_mem_dilatransvections
one_mem_transvections 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership transvections InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup	—	refl_mem_transvections
refl_mem_dilatransvections 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership dilatransvections refl	—	transvections_subset_dilatransvections one_mem_transvections
refl_mem_transvections 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership transvections refl	—	RingHomInvPair.ids transvection.of_left_eq_zero
symm_mem_dilatransvections_iff 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership dilatransvections symm	—	RingHomInvPair.ids LinearMap.ext sub_eq_iff_eq_add coe_coe LinearMap.transvection.apply smul_neg map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass apply_symm_apply
symm_mem_transvections_iff 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Set.instMembership transvections symm	—	RingHomInvPair.ids map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_zero transvection.symm_eq mem_transvections symm_symm
transvections_pow_mono 📖	mathematical	—	Monotone Set LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.NPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid transvections	—	Set.pow_right_monotone RingHomInvPair.ids one_mem_transvections
transvections_subset_dilatransvections 📖	mathematical	—	Set LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set.instHasSubset transvections dilatransvections	—	RingHomInvPair.ids

LinearEquiv.dilatransvection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Set Ring.toSemiring CommRing.toRing Set.instMembership LinearEquiv.dilatransvections	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.addCommGroup Ring.toAddCommGroup LinearEquiv.baseChange	—	RingHomInvPair.ids Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.transvection.baseChange

LinearEquiv.transvection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.transvection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids
baseChange 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Algebra.to_smulCommClass LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.id IsScalarTower.to_smulCommClass' IsScalarTower.right Module.Dual.baseChange TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	LinearEquiv.baseChange LinearEquiv.transvection TensorProduct.addCommGroup Ring.toAddCommGroup	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right RingHomInvPair.ids LinearMap.transvection.baseChange
coe_apply 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.transvection LinearMap LinearMap.transvection	—	RingHomInvPair.ids
coe_toLinearMap 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.transvection LinearMap.transvection	—	RingHomInvPair.ids
det_eq_one 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	MonoidHom LinearEquiv RingHomInvPair.ids Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det LinearEquiv.transvection CommRing.toRing Units.instOne	—	RingHomInvPair.ids LinearEquiv.coe_det coe_toLinearMap Units.val_one Module.Free.of_det_ne_one LinearMap.finite_of_det_ne_one LinearMap.transvection.det add_zero
inv_eq 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearEquiv RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearEquiv.automorphismGroup LinearEquiv.transvection	—	symm_eq map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_zero
inv_eq' 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instNeg Ring.toAddCommGroup	LinearEquiv RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearEquiv.automorphismGroup LinearEquiv.transvection	—	symm_eq' neg_zero
of_left_eq_zero 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.zero_apply	LinearEquiv.transvection LinearEquiv.refl	—	LinearEquiv.ext RingHomInvPair.ids LinearMap.transvection.of_left_eq_zero
of_right_eq_zero 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.map_zero	LinearEquiv.transvection LinearEquiv.refl	—	LinearEquiv.ext RingHomInvPair.ids LinearMap.transvection.of_right_eq_zero neg_zero
symm_eq 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LinearEquiv.symm RingHomInvPair.ids LinearEquiv.transvection	—	LinearEquiv.ext RingHomInvPair.ids LinearMap.transvection.comp_of_left_eq_apply add_neg_cancel LinearMap.transvection.of_right_eq_zero
symm_eq' 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instNeg Ring.toAddCommGroup	LinearEquiv.symm RingHomInvPair.ids LinearEquiv.transvection	—	LinearEquiv.ext RingHomInvPair.ids LinearMap.transvection.comp_of_right_eq_apply add_neg_cancel LinearMap.transvection.of_left_eq_zero
trans_of_left_eq 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	LinearEquiv.trans RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.transvection	—	LinearEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids LinearMap.transvection.comp_of_left_eq_apply
trans_of_right_eq 📖	mathematical	DFunLike.coe Module.Dual Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instAdd	LinearEquiv.trans RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.transvection	—	LinearEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids LinearMap.transvection.comp_of_right_eq_apply

LinearMap

Definitions

Name	Category	Theorems
transvection 📖	CompOp	14 math math: transvection.comp_of_left_eq_apply, transvection.comp_of_right_eq_apply, transvection.comp_of_left_eq, IsBaseChange.transvection, transvection.apply, transvection.of_right_eq_zero, transvection.eq_id_of_finrank_le_one, LinearEquiv.transvection.coe_apply, LinearEquiv.transvection.coe_toLinearMap, transvection.det, transvection.of_left_eq_zero, transvection.congr, transvection.comp_of_right_eq, transvection.baseChange

LinearMap.transvection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.transvection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—
baseChange 📖	mathematical	—	LinearMap.baseChange CommSemiring.toSemiring LinearMap.transvection TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass DFunLike.coe LinearMap RingHom.id Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.id IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instFunLike Module.Dual.baseChange TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.to_smulCommClass' LinearMap.ext_ring IsScalarTower.to_smulCommClass LinearMap.ext smulCommClass_self TensorProduct.tmul_add TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left smul_assoc one_smul
comp_of_left_eq 📖	mathematical	DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap.comp RingHomCompTriple.ids LinearMap.transvection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	LinearMap.ext RingHomCompTriple.ids comp_of_left_eq_apply
comp_of_left_eq_apply 📖	mathematical	DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap LinearMap.transvection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass zero_smul add_zero add_assoc smul_add
comp_of_right_eq 📖	mathematical	DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap.comp RingHomCompTriple.ids LinearMap.transvection LinearMap.instAdd	—	LinearMap.ext RingHomCompTriple.ids comp_of_right_eq_apply
comp_of_right_eq_apply 📖	mathematical	DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap LinearMap.transvection LinearMap.instAdd	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass zero_smul add_zero add_assoc add_smul
det 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearMap.transvection Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	subsingleton_or_nontrivial commRing_strongRankCondition AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsDomain IsScalarTower.of_compHom IsBaseChange.of_fintype_basis Fintype.linearCombination_apply_single one_smul Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.right Module.Basis.ext IsBaseChange.toDual_comp_apply RingHom.algebraMap_toAlgebra MvPolynomial.aeval_X RingHomInvPair.ids Finite.of_fintype IsBaseChange.of_fintype_basis_eq smulCommClass_self IsBaseChange.transvection IsBaseChange.det_endHom Module.Free.function Module.Free.self Module.Finite.pi Module.Finite.self map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AddLeftCancelSemigroup.toIsLeftCancelAdd
eq_id_of_finrank_le_one 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Module.finrank	LinearMap.transvection LinearMap.id	—	LinearMap.ext Nat.instZeroLEOneClass RingHomInvPair.ids Finite.of_fintype Module.Basis.sum_equivFun Finset.sum_eq_single_of_mem Finset.mem_univ map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_eq_mul SemigroupAction.mul_smul mul_assoc mul_comm MulZeroClass.mul_zero zero_smul add_zero le_antisymm Mathlib.Tactic.IntervalCases.of_le_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_ofNat Module.finrank_eq_zero_iff_of_free Subsingleton.eq_zero of_right_eq_zero LinearMap.identityMapOfZeroModuleIsZero
of_left_eq_zero 📖	mathematical	—	LinearMap.transvection Module.Dual LinearMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.id	—	LinearMap.ext zero_smul add_zero
of_right_eq_zero 📖	mathematical	—	LinearMap.transvection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.id	—	LinearMap.ext smul_zero add_zero

---

← Back to Index