Basic

📁 Source: Mathlib/LinearAlgebra/Transvection/Basic.lean

Statistics

Metric	Count
Definitions `dilatransvections`, `transvection`, `transvections`, `transvection`	4
Theorems `transvection`, `baseChange`, `dilatransvections_pow_mono`, `inv_mem_dilatransvections_iff`, `inv_mem_transvections_iff`, `ker_le_fixedSubmodule_transvection`, `mem_dilatransvections_iff_finrank`, `mem_dilatransvections_iff_finrank_quotient`, `mem_dilatransvections_iff_rank`, `mem_dilatransvections_iff_rank_quotient`, `mem_fixedSubmodule_transvection_iff`, `mem_transvections`, `mem_transvections_iff`, `mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one`, `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`, `transvection_mem_dilatransvections`, `transvection_mem_transvections`, `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`	47
Total	51

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	13 math math: `symm_mem_dilatransvections_iff`, `dilatransvections_pow_mono`, `mem_dilatransvections_iff_rank`, `transvections_subset_dilatransvections`, `transvection_mem_dilatransvections`, `mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one`, `mem_dilatransvections_iff_finrank`, `refl_mem_dilatransvections`, `mem_dilatransvections_iff_rank_quotient`, `one_mem_dilatransvections`, `dilatransvection.baseChange`, `inv_mem_dilatransvections_iff`, `mem_dilatransvections_iff_finrank_quotient`
`transvection` 📖	CompOp	19 math math: `transvection.det_eq_one`, `ker_le_fixedSubmodule_transvection`, `mem_fixedSubmodule_transvection_iff`, `mem_transvections_iff`, `transvection.apply`, `transvection_mem_dilatransvections`, `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_mem_transvections`, `transvection.symm_eq'`, `transvection.inv_eq`, `mem_transvections`
`transvections` 📖	CompOp	10 math math: `symm_mem_transvections_iff`, `one_mem_transvections`, `refl_mem_transvections`, `mem_transvections_iff`, `transvections_subset_dilatransvections`, `mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one`, `transvections_pow_mono`, `transvection_mem_transvections`, `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`
`ker_le_fixedSubmodule_transvection` 📖	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`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.fixedSubmodule` `toLinearMap` `RingHomInvPair.ids` `transvection`	—	`LinearMap.mem_ker` `zero_smul` `add_zero`
`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_finrank_quotient` 📖	mathematical	—	`LinearEquiv` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Ring.toSemiring` `DivisionRing.toRing` `Set.instMembership` `dilatransvections` `Module.finrank` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.fixedSubmodule` `toLinearMap` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`RingHomInvPair.ids` `RingHomSurjective.ids` `mem_dilatransvections_iff_finrank` `finrank_eq` `LinearMap.fixedSubmodule_eq_ker`
`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` `instReflLe` `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_dilatransvections_iff_rank_quotient` 📖	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` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.fixedSubmodule` `toLinearMap` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Cardinal.instOne`	—	`RingHomInvPair.ids` `RingHomSurjective.ids` `mem_dilatransvections_iff_rank` `rank_eq` `LinearMap.fixedSubmodule_eq_ker`
`mem_fixedSubmodule_transvection_iff` 📖	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`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearMap.fixedSubmodule` `toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `transvection` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Module.Dual` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `transvections` `transvection`	—	—
`mem_transvections_iff` 📖	mathematical	—	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `transvections` `Module.Dual` `DFunLike.coe` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `transvection`	—	`RingHomInvPair.ids`
`mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one` 📖	mathematical	—	`LinearEquiv` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Ring.toSemiring` `DivisionRing.toRing` `Set.instMembership` `transvections` `dilatransvections` `fixedReduce` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.fixedSubmodule` `toLinearMap` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `automorphismGroup`	—	`RingHomInvPair.ids` `transvection_mem_dilatransvections` `one_eq_refl` `fixedReduce_eq_one` `ker_le_fixedSubmodule_transvection` `transvection.apply` `add_sub_cancel_left` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MulZeroClass.mul_zero` `transvection.of_left_eq_zero` `fixedSubmodule_eq_top_iff` `SetLike.exists_not_mem_of_ne_top` `RingHomSurjective.ids` `Submodule.exists_dual_map_eq_bot_of_notMem` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Submodule.finrank_quotient_add_finrank` `DivisionRing.hasRankNullity` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Module.Dual.finrank_ker_add_one_of_ne_zero` `add_comm` `Submodule.eq_of_le_of_finrank_le` `FiniteDimensional.finiteDimensional_submodule` `LinearMap.mem_ker` `Submodule.mem_bot` `Submodule.mem_map_of_mem` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_add` `Nat.cast_one` `mem_dilatransvections_iff_finrank_quotient` `neg_eq_zero` `sub_eq_zero_of_eq` `Submodule.sup_span_singleton_eq_top_iff` `le_antisymm` `Mathlib.Tactic.Contrapose.contrapose₄` `Submodule.eq_top_of_finrank_eq` `zero_add` `Submodule.ker_mkQ` `sub_self` `LinearMap.map_smul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `smul_zero` `sub_eq_zero` `LinearMap.ker_eq_top` `eq_top_iff` `zero_smul` `add_zero` `smul_inv_smul₀` `add_sub_cancel`
`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`
`transvection_mem_dilatransvections` 📖	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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `dilatransvections` `transvection`	—	`transvections_subset_dilatransvections` `transvection_mem_transvections`
`transvection_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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `transvections` `transvection`	—	—
`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`	`LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Set` `Ring.toSemiring` `CommRing.toRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `Set.instMembership` `LinearEquiv.dilatransvections` `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`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `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` `Module.Dual` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`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` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearEquiv.transvection` `CommRing.toRing` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `Module.Dual` `TensorProduct.addCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.id` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `LinearMap.instFunLike` `Module.Dual.baseChange` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`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`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.transvection` `LinearMap` `LinearMap.instFunLike` `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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `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`	`DFunLike.coe` `MonoidHom` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearEquiv.automorphismGroup` `LinearEquiv.transvection` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`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` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearEquiv.automorphismGroup` `LinearEquiv.transvection` `Module.Dual` `LinearMap.instNeg` `Ring.toAddCommGroup` `Semiring.toModule`	—	`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` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instZero` `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` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `LinearEquiv.refl` `Ring.toSemiring`	—	`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` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.transvection` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`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` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.transvection` `Module.Dual` `LinearMap.instNeg` `Ring.toAddCommGroup` `Semiring.toModule`	—	`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` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.transvection` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`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` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.transvection` `Module.Dual` `LinearMap.instAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`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` `RingHom.id` `Semiring.toNonAssocSemiring` `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`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `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` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.transvection` `Module.Dual` `LinearMap.instAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`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`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.transvection` `Module.Dual` `LinearMap.instAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`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` `CommSemiring.toSemiring` `LinearMap.id`	—	`LinearMap.ext` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `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