Hom

📁 Source: Mathlib/LinearAlgebra/RootSystem/Hom.lean

Statistics

Metric	Count
Definitions `comp`, `coweightEquiv`, `coweightHom`, `id`, `indexHom`, `instDistribMulActionAut`, `instDistribMulActionMulOppositeAut`, `instGroup`, `instMonoid`, `instMulActionAut`, `mk'`, `reflection`, `toEndUnit`, `toHom`, `weightEquiv`, `weightHom`, `comp`, `coweightHom`, `coweightMap`, `id`, `indexEquiv`, `indexHom`, `instMonoid`, `weightHom`, `weightMap`	25
Theorems `bijective_coweightMap`, `bijective_weightMap`, `comp_assoc`, `comp_coweightMap_apply`, `comp_id`, `comp_indexEquiv_apply`, `comp_indexEquiv_symm_apply`, `comp_weightMap_apply`, `coweightEquiv_apply`, `coweightEquiv_comp_toLin`, `coweightEquiv_inv`, `coweightEquiv_mul`, `coweightEquiv_one`, `coweightEquiv_symm_coweightMap`, `coweightHom_apply`, `coweightHom_injective`, `coweightHom_op`, `coweightHom_toLinearMap`, `coweightMap_coweightEquiv_symm`, `ext`, `ext_iff`, `id_comp`, `id_coweightMap_apply`, `id_indexEquiv_apply`, `id_indexEquiv_symm_apply`, `id_weightMap_apply`, `indexEquiv_inv`, `indexHom_apply`, `instSMulCommClassAut`, `instSMulCommClassMulOppositeAut`, `inv_coweightMap`, `inv_indexEquiv`, `inv_weightMap`, `mul_eq_comp`, `reflection_coweightEquiv`, `reflection_indexEquiv`, `reflection_inv`, `reflection_smul`, `reflection_weightEquiv`, `root_indexEquiv_eq_smul`, `toEndUnit_inv`, `toEndUnit_val`, `toHom_comp`, `toHom_one`, `weightEquiv_apply`, `weightEquiv_comp_toLin`, `weightEquiv_inv`, `weightEquiv_mul`, `weightEquiv_one`, `weightEquiv_symm_weightMap`, `weightHom_apply`, `weightHom_injective`, `weightHom_toLinearMap`, `weightMap_weightEquiv_symm`, `comp_assoc`, `comp_coweightMap_apply`, `comp_id`, `comp_indexEquiv_apply`, `comp_indexEquiv_symm_apply`, `comp_weightMap_apply`, `coroot_coweightMap`, `coroot_coweightMap_apply`, `coweightHom_injective`, `coweightMap_mul`, `coweightMap_one`, `ext`, `ext_iff`, `id_comp`, `id_coweightMap_apply`, `id_indexEquiv_apply`, `id_indexEquiv_symm_apply`, `id_weightMap_apply`, `indexEquiv_mul`, `indexEquiv_one`, `root_weightMap`, `root_weightMap_apply`, `weightHom_injective`, `weightMap_mul`, `weightMap_one`, `weight_coweight_transpose`, `weight_coweight_transpose_apply`	81
Total	106

RootPairing.Equiv

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	11 math math: `coweightEquiv_comp_toLin`, `id_comp`, `comp_coweightMap_apply`, `comp_indexEquiv_apply`, `comp_weightMap_apply`, `comp_indexEquiv_symm_apply`, `comp_id`, `comp_assoc`, `mul_eq_comp`, `weightEquiv_comp_toLin`, `toHom_comp`
`coweightEquiv` 📖	CompOp	11 math math: `coweightEquiv_comp_toLin`, `coweightEquiv_symm_coweightMap`, `coweightEquiv_one`, `coweightEquiv_mul`, `coweightEquiv_inv`, `coweightMap_coweightEquiv_symm`, `coweightHom_op`, `inv_coweightMap`, `coweightHom_apply`, `reflection_coweightEquiv`, `coweightEquiv_apply`
`coweightHom` 📖	CompOp	5 math math: `RootPairing.range_weylGroup_coweightHom`, `coweightHom_injective`, `coweightHom_op`, `coweightHom_toLinearMap`, `coweightHom_apply`
`id` 📖	CompOp	6 math math: `id_coweightMap_apply`, `id_indexEquiv_apply`, `id_comp`, `comp_id`, `id_weightMap_apply`, `id_indexEquiv_symm_apply`
`indexHom` 📖	CompOp	2 math math: `indexHom_apply`, `indexEquiv_inv`
`instDistribMulActionAut` 📖	CompOp	7 math math: `RootPairing.span_orbit_eq_top`, `RootPairing.weylGroup_apply_root`, `root_indexEquiv_eq_smul`, `RootPairing.InvariantForm.apply_weylGroup_smul`, `instSMulCommClassAut`, `RootPairing.weylGroup.ofIdx_smul`, `reflection_smul`
`instDistribMulActionMulOppositeAut` 📖	CompOp	1 math math: `instSMulCommClassMulOppositeAut`
`instGroup` 📖	CompOp	15 math math: `RootPairing.weylGroup_toSubmonoid`, `RootPairing.span_orbit_eq_top`, `RootPairing.range_weylGroup_coweightHom`, `RootPairing.weylGroup_apply_root`, `weightEquiv_inv`, `coweightEquiv_inv`, `RootPairing.isSimpleModule_weylGroupRootRep`, `RootPairing.InvariantForm.apply_weylGroup_smul`, `RootPairing.isSimpleModule_weylGroupRootRep_iff`, `RootPairing.reflection_mem_weylGroup`, `RootPairing.range_weylGroupToPerm`, `RootPairing.weylGroup.ofIdx_smul`, `reflection_inv`, `RootPairing.range_weylGroup_weightHom`, `indexEquiv_inv`
`instMonoid` 📖	CompOp	24 math math: `toHom_one`, `RootPairing.weylGroup_toSubmonoid`, `RootPairing.range_weylGroup_coweightHom`, `weightHom_toLinearMap`, `toEndUnit_inv`, `RootPairing.weylGroup_apply_root`, `root_indexEquiv_eq_smul`, `coweightHom_injective`, `coweightEquiv_one`, `weightHom_apply`, `indexHom_apply`, `instSMulCommClassAut`, `RootPairing.weylGroup.ofIdx_smul`, `coweightHom_op`, `mul_eq_comp`, `weightEquiv_one`, `weightHom_injective`, `reflection_smul`, `RootPairing.range_weylGroup_weightHom`, `coweightHom_toLinearMap`, `instSMulCommClassMulOppositeAut`, `coweightHom_apply`, `indexEquiv_inv`, `toEndUnit_val`
`instMulActionAut` 📖	CompOp	—
`mk'` 📖	CompOp	—
`reflection` 📖	CompOp	8 math math: `RootPairing.weylGroup_toSubmonoid`, `RootPairing.reflection_mem_weylGroup`, `RootPairing.weylGroup.ofIdx_smul`, `reflection_inv`, `reflection_indexEquiv`, `reflection_smul`, `reflection_weightEquiv`, `reflection_coweightEquiv`
`toEndUnit` 📖	CompOp	2 math math: `toEndUnit_inv`, `toEndUnit_val`
`toHom` 📖	CompOp	30 math math: `id_coweightMap_apply`, `coweightEquiv_symm_coweightMap`, `toHom_one`, `id_indexEquiv_apply`, `weightHom_toLinearMap`, `toEndUnit_inv`, `inv_indexEquiv`, `root_indexEquiv_eq_smul`, `weightMap_weightEquiv_symm`, `comp_coweightMap_apply`, `weightEquiv_apply`, `comp_indexEquiv_apply`, `comp_weightMap_apply`, `comp_indexEquiv_symm_apply`, `bijective_weightMap`, `coweightMap_coweightEquiv_symm`, `bijective_coweightMap`, `indexHom_apply`, `weightEquiv_symm_weightMap`, `reflection_indexEquiv`, `id_weightMap_apply`, `ext_iff`, `inv_coweightMap`, `id_indexEquiv_symm_apply`, `toHom_comp`, `coweightHom_toLinearMap`, `indexEquiv_inv`, `toEndUnit_val`, `inv_weightMap`, `coweightEquiv_apply`
`weightEquiv` 📖	CompOp	10 math math: `weightMap_weightEquiv_symm`, `weightEquiv_apply`, `weightEquiv_mul`, `weightEquiv_inv`, `weightHom_apply`, `weightEquiv_one`, `weightEquiv_symm_weightMap`, `weightEquiv_comp_toLin`, `reflection_weightEquiv`, `inv_weightMap`
`weightHom` 📖	CompOp	4 math math: `weightHom_toLinearMap`, `weightHom_apply`, `weightHom_injective`, `RootPairing.range_weylGroup_weightHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_coweightMap` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom`	—	—
`bijective_weightMap` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext` `LinearMap.ext` `toHom_comp` `RootPairing.Hom.comp_assoc` `Equiv.ext`
`comp_coweightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom` `comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext` `LinearMap.ext` `toHom_comp` `Equiv.ext`
`comp_indexEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `RootPairing.Hom.indexEquiv` `toHom` `comp`	—	—
`comp_indexEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `RootPairing.Hom.indexEquiv` `toHom` `comp`	—	—
`comp_weightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom` `comp`	—	—
`coweightEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `coweightEquiv` `LinearMap` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom`	—	`RingHomInvPair.ids`
`coweightEquiv_comp_toLin` 📖	mathematical	—	`coweightEquiv` `comp` `LinearEquiv.trans` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `toHom_comp`
`coweightEquiv_inv` 📖	mathematical	—	`coweightEquiv` `RootPairing.Equiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.automorphismGroup`	—	`RingHomInvPair.ids`
`coweightEquiv_mul` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `coweightEquiv` `LinearEquiv.trans` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids`
`coweightEquiv_one` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `coweightEquiv` `RootPairing.Equiv` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.id`	—	`RingHomInvPair.ids`
`coweightEquiv_symm_coweightMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `coweightEquiv` `LinearMap` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom`	—	`RingHomInvPair.ids` `LinearEquiv.symm_apply_eq`
`coweightHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RootPairing.Aut` `MulOpposite` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulOpposite.instMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `coweightHom` `MulOpposite.op` `coweightEquiv`	—	`RingHomInvPair.ids`
`coweightHom_injective` 📖	mathematical	—	`RootPairing.Aut` `MulOpposite` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulOpposite.instMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `coweightHom`	—	`Function.Injective.of_comp` `RingHomInvPair.ids` `RootPairing.Hom.coweightHom_injective` `coweightHom_toLinearMap` `ext`
`coweightHom_op` 📖	mathematical	—	`MulOpposite.unop` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `RootPairing.Aut` `MulOpposite` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulOpposite.instMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `coweightHom` `coweightEquiv`	—	`RingHomInvPair.ids`
`coweightHom_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOpposite.unop` `LinearEquiv` `DFunLike.coe` `MonoidHom` `RootPairing.Aut` `MulOpposite` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulOpposite.instMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `coweightHom` `LinearMap` `RootPairing.End` `RootPairing.Hom.instMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `RootPairing.Hom.coweightHom` `toHom`	—	`RingHomInvPair.ids`
`coweightMap_coweightEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `coweightEquiv`	—	`RingHomInvPair.ids` `coweightEquiv_apply` `LinearEquiv.apply_symm_apply`
`ext` 📖	—	`RootPairing.Hom.weightMap` `toHom` `RootPairing.Hom.coweightMap` `RootPairing.Hom.indexEquiv`	—	—	`smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `RootPairing.isPerfPair_toLinearMap`
`ext_iff` 📖	mathematical	—	`RootPairing.Hom.weightMap` `toHom` `RootPairing.Hom.coweightMap` `RootPairing.Hom.indexEquiv`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext` `LinearMap.ext` `toHom_comp` `Equiv.ext`
`id_coweightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.coweightMap` `toHom` `id`	—	—
`id_indexEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `RootPairing.Hom.indexEquiv` `toHom` `id`	—	—
`id_indexEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `RootPairing.Hom.indexEquiv` `toHom` `id`	—	—
`id_weightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom` `id`	—	—
`indexEquiv_inv` 📖	mathematical	—	`RootPairing.Hom.indexEquiv` `toHom` `RootPairing.Aut` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `Equiv` `Equiv.Perm.instInv` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `indexHom`	—	—
`indexHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RootPairing.Aut` `Equiv` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `indexHom` `RootPairing.Hom.indexEquiv` `toHom`	—	—
`instSMulCommClassAut` 📖	mathematical	—	`SMulCommClass` `RootPairing.Aut` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `instDistribMulActionAut` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`instSMulCommClassMulOppositeAut` 📖	mathematical	—	`SMulCommClass` `MulOpposite` `RootPairing.Aut` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `instMonoid` `instDistribMulActionMulOppositeAut` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`inv_coweightMap` 📖	mathematical	—	`RootPairing.Hom.coweightMap` `toHom` `symm` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.symm` `coweightEquiv`	—	—
`inv_indexEquiv` 📖	mathematical	—	`RootPairing.Hom.indexEquiv` `toHom` `symm` `Equiv.symm`	—	—
`inv_weightMap` 📖	mathematical	—	`RootPairing.Hom.weightMap` `toHom` `symm` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.symm` `weightEquiv`	—	—
`mul_eq_comp` 📖	mathematical	—	`RootPairing.Equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `comp`	—	—
`reflection_coweightEquiv` 📖	mathematical	—	`coweightEquiv` `reflection` `RootPairing.coreflection`	—	`RingHomInvPair.ids`
`reflection_indexEquiv` 📖	mathematical	—	`RootPairing.Hom.indexEquiv` `toHom` `reflection` `RootPairing.reflectionPerm`	—	—
`reflection_inv` 📖	mathematical	—	`RootPairing.Aut` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `reflection`	—	`ext` `LinearMap.ext_iff` `RingHomInvPair.ids` `weightEquiv_inv` `reflection_weightEquiv` `coweightEquiv_inv` `reflection_coweightEquiv` `Equiv.ext` `RootPairing.reflectionPerm_inv`
`reflection_smul` 📖	mathematical	—	`RootPairing.Aut` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `instDistribMulActionAut` `reflection` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `RootPairing.reflection`	—	—
`reflection_weightEquiv` 📖	mathematical	—	`weightEquiv` `reflection` `RootPairing.reflection`	—	`RingHomInvPair.ids`
`root_indexEquiv_eq_smul` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `RootPairing.Hom.indexEquiv` `toHom` `RootPairing.Aut` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `instDistribMulActionAut`	—	`RootPairing.Hom.root_weightMap`
`toEndUnit_inv` 📖	mathematical	—	`Units.inv` `RootPairing.End` `RootPairing.Hom.instMonoid` `DFunLike.coe` `MulEquiv` `RootPairing.Aut` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toEndUnit` `toHom` `symm`	—	—
`toEndUnit_val` 📖	mathematical	—	`Units.val` `RootPairing.End` `RootPairing.Hom.instMonoid` `DFunLike.coe` `MulEquiv` `RootPairing.Aut` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toEndUnit` `toHom`	—	—
`toHom_comp` 📖	mathematical	—	`toHom` `comp` `RootPairing.Hom.comp`	—	—
`toHom_one` 📖	mathematical	—	`toHom` `RootPairing.Equiv` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `RootPairing.Hom` `RootPairing.Hom.instMonoid`	—	—
`weightEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `weightEquiv` `LinearMap` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom`	—	`RingHomInvPair.ids`
`weightEquiv_comp_toLin` 📖	mathematical	—	`weightEquiv` `comp` `LinearEquiv.trans` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `toHom_comp`
`weightEquiv_inv` 📖	mathematical	—	`weightEquiv` `RootPairing.Equiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.automorphismGroup`	—	`RingHomInvPair.ids`
`weightEquiv_mul` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `weightEquiv` `LinearEquiv.trans` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids`
`weightEquiv_one` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `weightEquiv` `RootPairing.Equiv` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.id`	—	`RingHomInvPair.ids`
`weightEquiv_symm_weightMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `weightEquiv` `LinearMap` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom`	—	`RingHomInvPair.ids` `LinearEquiv.symm_apply_eq`
`weightHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RootPairing.Aut` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `weightHom` `weightEquiv`	—	`RingHomInvPair.ids`
`weightHom_injective` 📖	mathematical	—	`RootPairing.Aut` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `weightHom`	—	`Function.Injective.of_comp` `RingHomInvPair.ids` `RootPairing.Hom.weightHom_injective` `ext`
`weightHom_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `RootPairing.Aut` `LinearEquiv` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `weightHom` `RootPairing.End` `Module.End` `RootPairing.Hom.instMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `RootPairing.Hom.weightHom` `toHom`	—	`RingHomInvPair.ids`
`weightMap_weightEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RootPairing.Hom.weightMap` `toHom` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `weightEquiv`	—	`RingHomInvPair.ids` `weightEquiv_apply` `LinearEquiv.apply_symm_apply`

RootPairing.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	8 math math: `comp_coweightMap_apply`, `comp_id`, `comp_indexEquiv_symm_apply`, `comp_indexEquiv_apply`, `comp_assoc`, `comp_weightMap_apply`, `id_comp`, `RootPairing.Equiv.toHom_comp`
`coweightHom` 📖	CompOp	2 math math: `coweightHom_injective`, `RootPairing.Equiv.coweightHom_toLinearMap`
`coweightMap` 📖	CompOp	17 math math: `RootPairing.Equiv.id_coweightMap_apply`, `comp_coweightMap_apply`, `RootPairing.Equiv.coweightEquiv_symm_coweightMap`, `coweightMap_mul`, `id_coweightMap_apply`, `weight_coweight_transpose`, `coweightMap_one`, `RootPairing.Equiv.comp_coweightMap_apply`, `coroot_coweightMap`, `ext_iff`, `RootPairing.Equiv.coweightMap_coweightEquiv_symm`, `RootPairing.Equiv.bijective_coweightMap`, `weight_coweight_transpose_apply`, `coroot_coweightMap_apply`, `RootPairing.Equiv.ext_iff`, `RootPairing.Equiv.inv_coweightMap`, `RootPairing.Equiv.coweightEquiv_apply`
`id` 📖	CompOp	6 math math: `id_coweightMap_apply`, `comp_id`, `id_weightMap_apply`, `id_comp`, `id_indexEquiv_apply`, `id_indexEquiv_symm_apply`
`indexEquiv` 📖	CompOp	21 math math: `root_weightMap`, `root_weightMap_apply`, `comp_indexEquiv_symm_apply`, `RootPairing.Equiv.id_indexEquiv_apply`, `RootPairing.Equiv.inv_indexEquiv`, `comp_indexEquiv_apply`, `indexEquiv_one`, `RootPairing.Equiv.root_indexEquiv_eq_smul`, `RootPairing.Equiv.comp_indexEquiv_apply`, `coroot_coweightMap`, `ext_iff`, `RootPairing.Equiv.comp_indexEquiv_symm_apply`, `indexEquiv_mul`, `RootPairing.Equiv.indexHom_apply`, `RootPairing.Equiv.reflection_indexEquiv`, `coroot_coweightMap_apply`, `RootPairing.Equiv.ext_iff`, `RootPairing.Equiv.id_indexEquiv_symm_apply`, `id_indexEquiv_apply`, `RootPairing.Equiv.indexEquiv_inv`, `id_indexEquiv_symm_apply`
`indexHom` 📖	CompOp	—
`instMonoid` 📖	CompOp	13 math math: `RootPairing.Equiv.toHom_one`, `coweightMap_mul`, `RootPairing.Equiv.weightHom_toLinearMap`, `RootPairing.Equiv.toEndUnit_inv`, `coweightMap_one`, `indexEquiv_one`, `coweightHom_injective`, `indexEquiv_mul`, `weightMap_one`, `weightMap_mul`, `RootPairing.Equiv.coweightHom_toLinearMap`, `weightHom_injective`, `RootPairing.Equiv.toEndUnit_val`
`weightHom` 📖	CompOp	2 math math: `RootPairing.Equiv.weightHom_toLinearMap`, `weightHom_injective`
`weightMap` 📖	CompOp	17 math math: `root_weightMap`, `root_weightMap_apply`, `weight_coweight_transpose`, `id_weightMap_apply`, `RootPairing.Equiv.weightMap_weightEquiv_symm`, `RootPairing.Equiv.weightEquiv_apply`, `comp_weightMap_apply`, `RootPairing.Equiv.comp_weightMap_apply`, `ext_iff`, `RootPairing.Equiv.bijective_weightMap`, `weightMap_one`, `weight_coweight_transpose_apply`, `RootPairing.Equiv.weightEquiv_symm_weightMap`, `RootPairing.Equiv.id_weightMap_apply`, `RootPairing.Equiv.ext_iff`, `weightMap_mul`, `RootPairing.Equiv.inv_weightMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext` `LinearMap.ext` `Equiv.ext`
`comp_coweightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `coweightMap` `comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext` `LinearMap.ext` `Equiv.ext`
`comp_indexEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `indexEquiv` `comp`	—	—
`comp_indexEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `indexEquiv` `comp`	—	—
`comp_weightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `weightMap` `comp`	—	—
`coroot_coweightMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `coweightMap` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.coroot` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `indexEquiv`	—	—
`coroot_coweightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `coweightMap` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.coroot` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `indexEquiv`	—	`coroot_coweightMap`
`coweightHom_injective` 📖	mathematical	—	`RootPairing.End` `MulOpposite` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulOpposite.instMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `coweightHom`	—	`ext` `LinearMap.ext` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `RootPairing.isPerfPair_toLinearMap` `smulCommClass_self` `Module.dualMap_dualMap_eq_iff` `Module.IsReflexive.of_isPerfPair` `LinearEquiv.eq_comp_toLinearMap_iff` `weight_coweight_transpose` `Equiv.Perm.ext` `Equiv.symm_apply_apply` `Function.Embedding.apply_eq_iff_eq` `coroot_coweightMap_apply` `Equiv.apply_symm_apply`
`coweightMap_mul` 📖	mathematical	—	`coweightMap` `RootPairing.Hom` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`coweightMap_one` 📖	mathematical	—	`coweightMap` `RootPairing.Hom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.id` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—
`ext` 📖	—	`weightMap` `coweightMap` `indexEquiv`	—	—	`smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `RootPairing.isPerfPair_toLinearMap`
`ext_iff` 📖	mathematical	—	`weightMap` `coweightMap` `indexEquiv`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext` `LinearMap.ext` `Equiv.ext`
`id_coweightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `coweightMap` `id`	—	—
`id_indexEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `indexEquiv` `id`	—	—
`id_indexEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `indexEquiv` `id`	—	—
`id_weightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `weightMap` `id`	—	—
`indexEquiv_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `indexEquiv` `RootPairing.Hom` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`indexEquiv_one` 📖	mathematical	—	`indexEquiv` `RootPairing.Hom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `Equiv.refl`	—	—
`root_weightMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `weightMap` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `indexEquiv`	—	—
`root_weightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `weightMap` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `indexEquiv`	—	`root_weightMap`
`weightHom_injective` 📖	mathematical	—	`RootPairing.End` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Module.End.instSemiring` `MonoidHom.instFunLike` `weightHom`	—	`ext` `LinearMap.ext` `LinearMap.congr_fun` `LinearEquiv.injective` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `RootPairing.isPerfPair_toLinearMap` `smulCommClass_self` `Equiv.Perm.ext` `Function.Embedding.injective`
`weightMap_mul` 📖	mathematical	—	`weightMap` `RootPairing.Hom` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`weightMap_one` 📖	mathematical	—	`weightMap` `RootPairing.Hom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `LinearMap.id` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—
`weight_coweight_transpose` 📖	mathematical	—	`LinearMap.comp` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `LinearMap.dualMap` `weightMap` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.toPerfPair` `RootPairing.toLinearMap` `RootPairing.flip` `RootPairing.isPerfPair_toLinearMap` `coweightMap`	—	—
`weight_coweight_transpose_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `LinearMap.dualMap` `weightMap` `LinearEquiv` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toPerfPair` `RootPairing.toLinearMap` `RootPairing.flip` `RootPairing.isPerfPair_toLinearMap` `coweightMap`	—	`smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `RootPairing.isPerfPair_toLinearMap` `LinearMap.ext_iff` `weight_coweight_transpose`

---

← Back to Index