Basic

📁 Source: Mathlib/Algebra/Module/Equiv/Basic.lean

Statistics

Metric	Count
Definitions toIntLinearEquiv, toLinearEquiv, toNatLinearEquiv, toLinearEquiv, toModuleAut, toLinearEquiv, applyDistribMulAction, arrowCongr, arrowCongrAddEquiv, automorphismGroup, toLinearMapMonoidHom, congrLeft, congrRight, conj, conjRingEquiv, curry, domMulActCongrRight, funCongrLeft, instUnique, instZero, neg, ofLinear, ofSubsingleton, piUnique, restrictScalars, smulOfNeZero, smulOfUnit, sumPiEquivProdPi, uniqueOfSubsingleton, funLeft, ringLmapEquivSelf, toLinearEquiv, addMonoidEndRingEquivInt, addMonoidHomLequivInt, addMonoidHomLequivNat	35
Theorems coe_symm_toIntLinearEquiv, coe_symm_toNatLinearEquiv, coe_toIntLinearEquiv, coe_toLinearEquiv, coe_toLinearEquiv_symm, coe_toNatLinearEquiv, toIntLinearEquiv_refl, toIntLinearEquiv_symm, toIntLinearEquiv_toAddEquiv, toIntLinearEquiv_trans, toNatLinearEquiv_refl, toNatLinearEquiv_symm, toNatLinearEquiv_toAddEquiv, toNatLinearEquiv_trans, toLinearEquiv_apply, toLinearEquiv_symm_apply, toModuleAut_apply, apply_faithfulSMul, apply_smulCommClass, apply_smulCommClass', arrowCongrAddEquiv_apply, arrowCongrAddEquiv_symm_apply, arrowCongr_apply, arrowCongr_comp, arrowCongr_symm_apply, arrowCongr_trans, toLinearMapMonoidHom_apply, coe_curry, coe_curry_symm, coe_inv, coe_neg, coe_one, coe_pow, coe_toLinearMap_mul, coe_toLinearMap_one, coe_zero, congrLeft_apply, congrLeft_symm_apply, conjRingEquiv_apply_apply, conjRingEquiv_symm_apply_apply, conj_apply, conj_apply_apply, conj_comp, conj_conj_symm, conj_id, conj_refl, conj_symm_conj, conj_trans, domMulActCongrRight_apply, domMulActCongrRight_symm_apply, funCongrLeft_apply, funCongrLeft_comp, funCongrLeft_id, funCongrLeft_symm, mul_apply, mul_eq_trans, neg_apply, ofLinear_apply, ofLinear_symm_apply, ofLinear_symm_toLinearMap, ofLinear_toLinearMap, ofSubsingleton_apply, ofSubsingleton_self, ofSubsingleton_symm_apply, one_eq_refl, piUnique_apply, piUnique_symm_apply, pow_apply, restrictScalars_apply, restrictScalars_inj, restrictScalars_injective, restrictScalars_symm_apply, smulOfNeZero_apply, smulOfNeZero_symm_apply, smul_def, smul_refl, sumPiEquivProdPi_apply, sumPiEquivProdPi_symm_apply, symm_conj_apply, symm_neg, toAddEquiv_toIntLinearEquiv, toAddEquiv_toNatLinearEquiv, zero_apply, zero_symm, funLeft_apply, funLeft_comp, funLeft_id, funLeft_injective_of_surjective, funLeft_surjective_of_injective, ringLmapEquivSelf_apply, ringLmapEquivSelf_symm_apply, isUnit_iff, toLinearEquiv_apply, toLinearEquiv_symm_apply, addMonoidEndRingEquivInt_apply, addMonoidEndRingEquivInt_symm_apply, addMonoidHomLequivInt_apply, addMonoidHomLequivInt_symm_apply, addMonoidHomLequivNat_apply, addMonoidHomLequivNat_symm_apply	100
Total	135

AddEquiv

Definitions

Name	Category	Theorems
toIntLinearEquiv 📖	CompOp	7 math math: toIntLinearEquiv_toAddEquiv, toIntLinearEquiv_refl, toIntLinearEquiv_trans, toIntLinearEquiv_symm, coe_toIntLinearEquiv, LinearEquiv.toAddEquiv_toIntLinearEquiv, coe_symm_toIntLinearEquiv
toLinearEquiv 📖	CompOp	2 math math: coe_toLinearEquiv_symm, coe_toLinearEquiv
toNatLinearEquiv 📖	CompOp	7 math math: toNatLinearEquiv_toAddEquiv, toNatLinearEquiv_trans, toNatLinearEquiv_refl, coe_symm_toNatLinearEquiv, coe_toNatLinearEquiv, LinearEquiv.toAddEquiv_toNatLinearEquiv, toNatLinearEquiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_symm_toIntLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toIntLinearEquiv AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instEquivLike symm	—	RingHomInvPair.ids
coe_symm_toNatLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv Nat.instSemiring RingHom.id Semiring.toNonAssocSemiring Nat.instNonAssocSemiring RingHomInvPair.ids AddCommMonoid.toNatModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toNatLinearEquiv AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instEquivLike symm	—	RingHomInvPair.ids
coe_toIntLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike toIntLinearEquiv AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instEquivLike	—	RingHomInvPair.ids
coe_toLinearEquiv 📖	mathematical	DFunLike.coe AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike instEquivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.instEquivLike toLinearEquiv	—	RingHomInvPair.ids
coe_toLinearEquiv_symm 📖	mathematical	DFunLike.coe AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike instEquivLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv symm	—	RingHomInvPair.ids
coe_toNatLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv Nat.instSemiring RingHom.id Nat.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommMonoid.toNatModule EquivLike.toFunLike LinearEquiv.instEquivLike toNatLinearEquiv AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instEquivLike	—	RingHomInvPair.ids
toIntLinearEquiv_refl 📖	mathematical	—	toIntLinearEquiv refl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearEquiv.refl Int.instSemiring	—	RingHomInvPair.ids
toIntLinearEquiv_symm 📖	mathematical	—	toIntLinearEquiv symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearEquiv.symm Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
toIntLinearEquiv_toAddEquiv 📖	mathematical	—	AddEquivClass.toAddEquiv LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid LinearEquiv.instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass toIntLinearEquiv	—	ext RingHomInvPair.ids SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
toIntLinearEquiv_trans 📖	mathematical	—	toIntLinearEquiv trans AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearEquiv.trans Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids	—	RingHomInvPair.ids
toNatLinearEquiv_refl 📖	mathematical	—	toNatLinearEquiv refl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearEquiv.refl Nat.instSemiring AddCommMonoid.toNatModule	—	RingHomInvPair.ids
toNatLinearEquiv_symm 📖	mathematical	—	toNatLinearEquiv symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearEquiv.symm Nat.instSemiring AddCommMonoid.toNatModule RingHom.id Nat.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
toNatLinearEquiv_toAddEquiv 📖	mathematical	—	AddEquivClass.toAddEquiv LinearEquiv Nat.instSemiring RingHom.id Nat.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommMonoid.toNatModule LinearEquiv.instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass toNatLinearEquiv	—	RingHomInvPair.ids SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
toNatLinearEquiv_trans 📖	mathematical	—	toNatLinearEquiv trans AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearEquiv.trans Nat.instSemiring AddCommMonoid.toNatModule RingHom.id Nat.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids	—	RingHomInvPair.ids

DistribMulAction

Definitions

Name	Category	Theorems
toLinearEquiv 📖	CompOp	7 math math: toModuleAut_apply, toLinearEquiv_symm_apply, Module.Basis.repr_smul, toLinearEquiv_apply, AffineBasis.coord_smul, ContinuousLinearEquiv.smulLeft_apply_toLinearEquiv, LinearEquiv.smul_refl
toModuleAut 📖	CompOp	1 math math: toModuleAut_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	—	RingHomInvPair.ids
toLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction toMulAction AddCommMonoid.toAddMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids
toModuleAut_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MonoidHom.instFunLike toModuleAut toLinearEquiv	—	RingHomInvPair.ids

Equiv

Definitions

Name	Category	Theorems
toLinearEquiv 📖	CompOp	—

LinearEquiv

Definitions

Name	Category	Theorems
applyDistribMulAction 📖	CompOp	8 math math: RootPairing.mem_range_root_of_mem_range_reflection_of_mem_range_root, Module.Ray.linearEquiv_smul_eq_map, RootPairing.mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot, apply_smulCommClass, Module.Basis.smul_eq_map, apply_smulCommClass', smul_def, apply_faithfulSMul
arrowCongr 📖	CompOp	13 math math: LinearMap.Nondegenerate.congr, ModuleCat.Iso.homCongr_eq_arrowCongr, SemimoduleCat.Iso.homCongr_eq_arrowCongr, LinearMap.separatingRight_congr_iff, arrowCongr_symm_apply, LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr, LinearMap.SeparatingRight.congr, arrowCongr_apply, LinearMap.nondegenerate_congr_iff, LinearMap.separatingLeft_congr_iff, arrowCongr_trans, arrowCongr_comp, LinearMap.SeparatingLeft.congr
arrowCongrAddEquiv 📖	CompOp	6 math math: domMulActCongrRight_symm_apply, domMulActCongrRight_apply, congrLeft_symm_apply, congrLeft_apply, arrowCongrAddEquiv_apply, arrowCongrAddEquiv_symm_apply
automorphismGroup 📖	CompOp	129 math math: DistribMulAction.toModuleAut_apply, lTensor_pow, Complex.linearEquiv_det_conjLIE, Orientation.linearEquiv_det_rotation, transvection.det_eq_one, det_trans, ZLattice.covolume_eq_det_inv, SpecialLinearGroup.coe_zpow, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, SpecialLinearGroup.mem_center_iff_spec, SpecialLinearGroup.mem_center_iff, RootPairing.range_weylGroup_coweightHom, coe_inv, SpecialLinearGroup.coe_one, dilatransvections_pow_mono, rTensor_mul, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, Module.reflection_inv, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, RootPairing.Equiv.weightHom_toLinearMap, one_mem_transvections, det_baseChange, coe_toLinearMap_mul, TensorProduct.congr_zpow, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, RootPairing.mem_range_root_of_mem_range_reflection_of_mem_range_root, mul_eq_trans, lTensor_zpow, ModularGroup.lcRow0Extend_symm_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, RootPairing.coreflection_inv, rTensor_zpow, Module.Ray.linearEquiv_smul_eq_map, isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo, Module.reflection_mul_reflection_pow_apply, RootPairing.Equiv.coweightHom_injective, LinearMap.GeneralLinearGroup.ofLinearEquiv_inv, coe_pow, RootPairing.mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot, SpecialLinearGroup.coe_inv, mul_apply, RootPairing.reflection_sq, SpecialLinearGroup.congr_linearEquiv_coe_apply, SpecialLinearGroup.det_eq_one, ModularGroup.lcRow0Extend_apply, LinearMap.GeneralLinearGroup.toLinearEquiv_inv, Submodule.linearEquiv_det_reflection, rTensor_pow, TensorProduct.AlgebraTensorModule.congr_mul, baseChange_mul, Orientation.map_eq_det_inv_smul, Module.reflection_mul_reflection_pow, RootPairing.Equiv.weightEquiv_mul, det_symm, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, SpecialLinearGroup.det_coe, RootPairing.Equiv.weightEquiv_inv, RootPairing.Equiv.coweightEquiv_mul, apply_smulCommClass, RootPairing.Equiv.coweightEquiv_inv, baseChange_zpow, SpecialLinearGroup.coe_mul, transvections_pow_mono, det_conj, RootPairing.Equiv.weightHom_apply, SpecialLinearGroup.coe_pow, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, AffineEquiv.linearHom_apply, Module.reflection_mul_reflection_pow_apply_self, Complex.linearEquiv_det_conjAe, Module.Basis.smul_eq_map, SpecialLinearGroup.centerEquivRootsOfUnity_apply, one_mem_dilatransvections, SpecialLinearGroup.toLinearEquiv_symm_apply, apply_smulCommClass', RootPairing.coreflection_sq, baseChange_inv, RootPairing.Equiv.coweightHom_op, linearEquiv_det_rotation, Matrix.SpecialLinearGroup.toLin'_to_linearMap, TensorProduct.congr_mul, Module.Basis.map_orientation_eq_det_inv_smul, inv_mem_dilatransvections_iff, Module.reflection_mul_reflection_zpow_apply_self, RootPairing.Equiv.weightHom_injective, TensorProduct.AlgebraTensorModule.congr_one, Module.reflection_mul_reflection_zpow_apply, Polynomial.det_taylorLinearEquiv, smul_def, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, RootPairing.reflection_inv, coe_inv_det, LinearMap.GeneralLinearGroup.toLinearEquiv_mul, transvection.inv_eq', Matrix.SpecialLinearGroup.toLin'_injective, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, baseChange_pow, coe_one, LinearMap.GeneralLinearGroup.ofLinearEquiv_mul, TensorProduct.congr_pow, pow_apply, Matrix.SpecialLinearGroup.toLin'_symm_apply, automorphismGroup.toLinearMapMonoidHom_apply, one_eq_refl, inv_mem_transvections_iff, RootPairing.range_weylGroup_weightHom, baseChange_one, det_refl, SpecialLinearGroup.baseChange_apply_coe, RootPairing.isOrthogonal_comm, RootPairing.Equiv.coweightHom_toLinearMap, SpecialLinearGroup.coe_div, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, SpecialLinearGroup.toLinearEquiv_injective, RootPairing.Equiv.coweightHom_apply, RootPairing.reflection_reflectionPerm, SpecialLinearGroup.coe_dualMap, transvection.inv_eq, Module.reflection_mul_reflection_mul_reflection_pow_apply_self, Module.reflection_mul_reflection_mul_reflection_zpow_apply_self, coe_toLinearMap_one, Module.reflection_mul_reflection_zpow, lTensor_mul, SpecialLinearGroup.toLinearEquiv_to_linearMap, Matrix.SpecialLinearGroup.toLin'_apply, coe_det, apply_faithfulSMul, SpecialLinearGroup.toLinearEquiv_apply
congrLeft 📖	CompOp	2 math math: congrLeft_symm_apply, congrLeft_apply
congrRight 📖	CompOp	1 math math: Module.Invertible.rTensorEquiv_symm_apply_apply
conj 📖	CompOp	28 math math: conj_trans, conj_apply_apply, map_mem_invtSubmodule_conj_iff, AlgEquiv.linearEquivConj_mulLeft, LieModule.shiftedGenWeightSpace.toEnd_eq, conj_comp, conj_refl, LinearMap.IsProj.eq_conj_prodMap, conj_apply, conj_symm_conj, lieConj_apply, LinearMap.isPairSelfAdjoint_equiv, FGModuleCat.Iso.conj_eq_conj, LieAlgebra.conj_ad_apply, AlgEquiv.linearEquivConj_mulLeftRight, symm_conj_apply, conj_conj_symm, SemimoduleCat.Iso.conj_eq_conj, LinearMap.trace_conj', conj_id, RootPairing.toPerfPair_conj_reflection, charpoly_conj, AlgEquiv.linearEquivConj_mulRight, ModuleCat.Iso.conj_eq_conj, RootPairing.toPerfPair_flip_conj_coreflection, FDRep.Iso.conj_ρ, map_mem_invtSubmodule_iff, FGModuleCat.Iso.conj_hom_eq_conj
conjRingEquiv 📖	CompOp	2 math math: conjRingEquiv_apply_apply, conjRingEquiv_symm_apply_apply
curry 📖	CompOp	2 math math: coe_curry, coe_curry_symm
domMulActCongrRight 📖	CompOp	2 math math: domMulActCongrRight_symm_apply, domMulActCongrRight_apply
funCongrLeft 📖	CompOp	6 math math: funCongrLeft_apply, Matrix.toLin'_reindex, funCongrLeft_id, Matrix.mulVecLin_reindex, funCongrLeft_comp, funCongrLeft_symm
instUnique 📖	CompOp	—
instZero 📖	CompOp	3 math math: zero_symm, zero_apply, coe_zero
neg 📖	CompOp	3 math math: coe_neg, symm_neg, neg_apply
ofLinear 📖	CompOp	4 math math: ofLinear_toLinearMap, ofLinear_symm_apply, ofLinear_symm_toLinearMap, ofLinear_apply
ofSubsingleton 📖	CompOp	3 math math: ofSubsingleton_apply, ofSubsingleton_self, ofSubsingleton_symm_apply
piUnique 📖	CompOp	2 math math: piUnique_symm_apply, piUnique_apply
restrictScalars 📖	CompOp	8 math math: extendScalarsOfIsLocalizationEquiv_symm_apply, restrictScalars_apply, restrictScalars_symm_apply, ZSpan.map, restrictScalars_injective, TensorProduct.directSumRight'_restrict, restrictScalars_inj, Module.Basis.mapCoeffs_repr
smulOfNeZero 📖	CompOp	2 math math: smulOfNeZero_apply, smulOfNeZero_symm_apply
smulOfUnit 📖	CompOp	—
sumPiEquivProdPi 📖	CompOp	2 math math: sumPiEquivProdPi_apply, sumPiEquivProdPi_symm_apply
uniqueOfSubsingleton 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_faithfulSMul 📖	mathematical	—	FaithfulSMul LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup applyDistribMulAction	—	RingHomInvPair.ids ext
apply_smulCommClass 📖	mathematical	—	SMulCommClass LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup applyDistribMulAction	—	RingHomInvPair.ids LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul
apply_smulCommClass' 📖	mathematical	—	SMulCommClass LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup applyDistribMulAction	—	SMulCommClass.symm RingHomInvPair.ids apply_smulCommClass
arrowCongrAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv LinearMap LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike arrowCongrAddEquiv LinearMap.comp toLinearMap symm	—	—
arrowCongrAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv LinearMap LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm arrowCongrAddEquiv LinearMap.comp toLinearMap symm	—	—
arrowCongr_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearEquiv LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike arrowCongr symm	—	smulCommClass_self
arrowCongr_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike arrowCongr LinearMap.comp	—	LinearMap.ext smulCommClass_self symm_apply_apply
arrowCongr_symm_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearEquiv LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike symm arrowCongr	—	smulCommClass_self
arrowCongr_trans 📖	mathematical	—	trans LinearMap CommSemiring.toSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction arrowCongr	—	smulCommClass_self
coe_curry 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike instEquivLike curry	—	RingHomInvPair.ids
coe_curry_symm 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike instEquivLike symm curry	—	RingHomInvPair.ids
coe_inv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup symm	—	RingHomInvPair.ids
coe_neg 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike neg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomInvPair.ids
coe_one 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup	—	RingHomInvPair.ids
coe_pow 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Nat.iterate	—	RingHomInvPair.ids hom_coe_pow
coe_toLinearMap_mul 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup LinearMap Module.End.instMul	—	RingHomInvPair.ids
coe_toLinearMap_one 📖	mathematical	—	toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup LinearMap.id	—	RingHomInvPair.ids
coe_zero 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
congrLeft_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module EquivLike.toFunLike instEquivLike congrLeft Equiv.toFun AddEquiv.toEquiv LinearMap.instAdd arrowCongrAddEquiv refl	—	RingHomInvPair.ids
congrLeft_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module EquivLike.toFunLike instEquivLike symm congrLeft Equiv.invFun AddEquiv.toEquiv LinearMap.instAdd arrowCongrAddEquiv refl	—	RingHomInvPair.ids
conjRingEquiv_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike RingEquiv Module.End Module.End.instMul LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike conjRingEquiv LinearEquiv instEquivLike symm	—	—
conjRingEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike RingEquiv Module.End Module.End.instMul LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm conjRingEquiv LinearEquiv instEquivLike symm	—	—
conj_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj LinearMap.comp RingHomInvPair.triples₂ RingHomCompTriple.ids toLinearMap symm	—	smulCommClass_self
conj_apply_apply 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearEquiv LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj symm	—	smulCommClass_self
conj_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj LinearMap.comp RingHomCompTriple.ids	—	arrowCongr_comp RingHomCompTriple.ids RingHomInvPair.triples₂
conj_conj_symm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj symm	—	LinearMap.ext smulCommClass_self apply_symm_apply
conj_id 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj LinearMap.id	—	LinearMap.ext smulCommClass_self apply_symm_apply
conj_refl 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.End LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj refl	—	RingHomInvPair.ids smulCommClass_self
conj_symm_conj 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj symm	—	LinearMap.ext smulCommClass_self symm_apply_apply
conj_trans 📖	mathematical	—	trans Module.End CommSemiring.toSemiring LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction conj	—	smulCommClass_self
domMulActCongrRight_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DomMulAct DomMulAct.instSemiringOfMulOpposite MulOpposite.instSemiring RingHom.id DomMulAct.instNonAssocSemiringOfMulOpposite MulOpposite.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.instModuleDomMulActOfSMulCommClass EquivLike.toFunLike instEquivLike domMulActCongrRight Equiv.toFun AddEquiv.toEquiv LinearMap.instAdd arrowCongrAddEquiv RingHomCompTriple.ids refl	—	RingHomInvPair.ids
domMulActCongrRight_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DomMulAct DomMulAct.instSemiringOfMulOpposite MulOpposite.instSemiring RingHom.id Semiring.toNonAssocSemiring DomMulAct.instNonAssocSemiringOfMulOpposite MulOpposite.instNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.instModuleDomMulActOfSMulCommClass EquivLike.toFunLike instEquivLike symm domMulActCongrRight Equiv.invFun AddEquiv.toEquiv LinearMap.instAdd arrowCongrAddEquiv RingHomCompTriple.ids refl	—	RingHomInvPair.ids
funCongrLeft_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike instEquivLike funCongrLeft LinearMap LinearMap.instFunLike LinearMap.funLeft Equiv Equiv.instEquivLike	—	RingHomInvPair.ids
funCongrLeft_comp 📖	mathematical	—	funCongrLeft Equiv.trans trans Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids	—	RingHomInvPair.ids
funCongrLeft_id 📖	mathematical	—	funCongrLeft Equiv.refl refl Pi.addCommMonoid Pi.Function.module	—	RingHomInvPair.ids
funCongrLeft_symm 📖	mathematical	—	symm Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids funCongrLeft Equiv.symm	—	RingHomInvPair.ids
mul_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup	—	RingHomInvPair.ids
mul_eq_trans 📖	mathematical	—	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup trans RingHomCompTriple.ids	—	RingHomInvPair.ids
neg_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
ofLinear_apply 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearMap.id	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike ofLinear LinearMap LinearMap.instFunLike	—	RingHomInvPair.triples₂
ofLinear_symm_apply 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearMap.id	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike symm ofLinear LinearMap LinearMap.instFunLike	—	RingHomInvPair.triples₂
ofLinear_symm_toLinearMap 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearMap.id	toLinearMap symm ofLinear	—	RingHomInvPair.triples₂
ofLinear_toLinearMap 📖	mathematical	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.triples₂ LinearMap.id	toLinearMap ofLinear	—	RingHomInvPair.triples₂
ofSubsingleton_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike ofSubsingleton AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
ofSubsingleton_self 📖	mathematical	—	ofSubsingleton refl	—	ext RingHomInvPair.ids
ofSubsingleton_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm ofSubsingleton AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
one_eq_refl 📖	mathematical	—	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid automorphismGroup refl	—	RingHomInvPair.ids
piUnique_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Unique.instInhabited Pi.addCommMonoid Pi.module EquivLike.toFunLike instEquivLike piUnique Equiv.toFun Equiv.piUnique	—	RingHomInvPair.ids
piUnique_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Unique.instInhabited Pi.addCommMonoid Pi.module EquivLike.toFunLike instEquivLike symm piUnique Equiv.invFun Equiv.piUnique	—	RingHomInvPair.ids
pow_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Nat.iterate	—	RingHomInvPair.ids coe_pow
restrictScalars_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike restrictScalars	—	RingHomInvPair.ids
restrictScalars_inj 📖	mathematical	—	restrictScalars	—	RingHomInvPair.ids restrictScalars_injective
restrictScalars_injective 📖	mathematical	—	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids restrictScalars	—	RingHomInvPair.ids ext congr_fun
restrictScalars_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike symm restrictScalars	—	RingHomInvPair.ids
smulOfNeZero_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike smulOfNeZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Module.toDistribMulAction	—	RingHomInvPair.ids
smulOfNeZero_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike symm smulOfNeZero Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instGroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Units.instDistribMulAction Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	RingHomInvPair.ids
smul_def 📖	mathematical	—	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup applyDistribMulAction DFunLike.coe EquivLike.toFunLike instEquivLike	—	RingHomInvPair.ids
smul_refl 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instSMulUnitsId refl DistribMulAction.toLinearEquiv Units.instGroup Units.instDistribMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Units.instSMul Units.smulCommClass_right	—	RingHomInvPair.ids
sumPiEquivProdPi_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.module Prod.instModule EquivLike.toFunLike instEquivLike sumPiEquivProdPi Equiv Equiv.instEquivLike Equiv.sumPiEquivProdPi	—	RingHomInvPair.ids
sumPiEquivProdPi_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.module EquivLike.toFunLike instEquivLike symm sumPiEquivProdPi Equiv Equiv.instEquivLike Equiv.symm Equiv.sumPiEquivProdPi	—	RingHomInvPair.ids
symm_conj_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj symm LinearMap.comp RingHomInvPair.triples₂ RingHomCompTriple.ids toLinearMap	—	smulCommClass_self
symm_neg 📖	mathematical	—	symm AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids neg	—	RingHomInvPair.ids
toAddEquiv_toIntLinearEquiv 📖	mathematical	—	AddEquiv.toIntLinearEquiv AddEquivClass.toAddEquiv LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass	—	RingHomInvPair.ids DFunLike.coe_injective SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass
toAddEquiv_toNatLinearEquiv 📖	mathematical	—	AddEquiv.toNatLinearEquiv AddEquivClass.toAddEquiv LinearEquiv Nat.instSemiring RingHom.id Nat.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommMonoid.toNatModule instEquivLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass	—	RingHomInvPair.ids DFunLike.coe_injective SemilinearEquivClass.toAddEquivClass instSemilinearEquivClass
zero_apply 📖	mathematical	—	DFunLike.coe LinearEquiv EquivLike.toFunLike instEquivLike instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
zero_symm 📖	mathematical	—	symm LinearEquiv instZero	—	—

LinearEquiv.automorphismGroup

Definitions

Name	Category	Theorems
toLinearMapMonoidHom 📖	CompOp	1 math math: toLinearMapMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearMapMonoidHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike toLinearMapMonoidHom LinearEquiv.toLinearMap	—	RingHomInvPair.ids

LinearMap

Definitions

Name	Category	Theorems
funLeft 📖	CompOp	16 math math: funLeft_id, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, funLeft_comp, funLeft_surjective_of_injective, LinearEquiv.funCongrLeft_apply, funLeft_injective_of_surjective, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.cochainsMap_f, Matrix.mulVecLin_submatrix, groupCohomology.mapCocycles₁_comp_i_apply, Matrix.toLin'_submatrix, groupCohomology.cochainsMap_f_hom, funLeft_apply, Representation.coind_apply
ringLmapEquivSelf 📖	CompOp	2 math math: ringLmapEquivSelf_symm_apply, ringLmapEquivSelf_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
funLeft_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike funLeft	—	—
funLeft_comp 📖	mathematical	—	funLeft comp Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
funLeft_id 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike funLeft	—	—
funLeft_injective_of_surjective 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike funLeft	—	Function.Surjective.injective_comp_right
funLeft_surjective_of_injective 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike funLeft	—	Function.Injective.surjective_comp_right Zero.instNonempty
ringLmapEquivSelf_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike ringLmapEquivSelf instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
ringLmapEquivSelf_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm ringLmapEquivSelf smulRight Module.End.instOne	—	RingHomInvPair.ids

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_iff 📖	mathematical	—	IsUnit Module.End instMonoid Function.Bijective DFunLike.coe LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	—	Function.bijective_iff_has_inverse isUnit_inv_apply_apply_of_isUnit isUnit_apply_inv_apply_of_isUnit RingHomInvPair.ids Equiv.left_inv Equiv.right_inv LinearMap.ext LinearEquiv.right_inv LinearEquiv.left_inv

Module.compHom

Definitions

Name	Category	Theorems
toLinearEquiv 📖	CompOp	3 math math: Module.Basis.mapCoeffs_repr, toLinearEquiv_symm_apply, toLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Module.compHom RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass LinearEquiv.instEquivLike toLinearEquiv	—	RingHomInvPair.ids RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
toLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Module.compHom Semiring.toModule RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv RingEquiv.symm	—	RingHomInvPair.ids RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass

(root)

Definitions

Name	Category	Theorems
addMonoidEndRingEquivInt 📖	CompOp	2 math math: addMonoidEndRingEquivInt_apply, addMonoidEndRingEquivInt_symm_apply
addMonoidHomLequivInt 📖	CompOp	4 math math: addMonoidHomLequivInt_apply, addMonoidEndRingEquivInt_apply, addMonoidHomLequivInt_symm_apply, addMonoidEndRingEquivInt_symm_apply
addMonoidHomLequivNat 📖	CompOp	2 math math: addMonoidHomLequivNat_symm_apply, addMonoidHomLequivNat_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addMonoidEndRingEquivInt_apply 📖	mathematical	—	DFunLike.coe RingEquiv AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.End Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoid.End.instMul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoid.End.instRing LinearMap.instAdd RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike addMonoidEndRingEquivInt AddHom.toFun AddMonoidHom LinearMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoidHom.instAddCommMonoid LinearMap.addCommMonoid LinearMap.toAddHom AddMonoidHom.instModule LinearMap.module LinearEquiv.toLinearMap RingHomInvPair.ids addMonoidHomLequivInt	—	—
addMonoidEndRingEquivInt_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Module.End Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.End.instMul AddMonoid.End.instMul LinearMap.instAdd RingHom.id Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoid.End.instRing EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm addMonoidEndRingEquivInt LinearEquiv.invFun RingHomInvPair.ids AddMonoidHom LinearMap AddMonoidHom.instAddCommMonoid LinearMap.addCommMonoid AddMonoidHom.instModule LinearMap.module addMonoidHomLequivInt	—	—
addMonoidHomLequivInt_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoidHom.instAddCommMonoid LinearMap.addCommMonoid AddMonoidHom.instModule LinearMap.module AddGroup.int_smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike addMonoidHomLequivInt AddMonoidHom.toIntLinearMap	—	RingHomInvPair.ids AddGroup.int_smulCommClass
addMonoidHomLequivInt_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommMonoid AddMonoidHom.instAddCommMonoid LinearMap.module AddGroup.int_smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidHom.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm addMonoidHomLequivInt LinearMap.toAddMonoidHom	—	RingHomInvPair.ids AddGroup.int_smulCommClass
addMonoidHomLequivNat_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap Nat.instSemiring Nat.instNonAssocSemiring AddCommMonoid.toNatModule AddMonoidHom.instAddCommMonoid LinearMap.addCommMonoid AddMonoidHom.instModule LinearMap.module AddMonoid.nat_smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike addMonoidHomLequivNat AddMonoidHom.toNatLinearMap	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass
addMonoidHomLequivNat_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Nat.instSemiring Nat.instNonAssocSemiring AddCommMonoid.toNatModule AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.addCommMonoid AddMonoidHom.instAddCommMonoid LinearMap.module AddMonoid.nat_smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidHom.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm addMonoidHomLequivNat LinearMap.toAddMonoidHom	—	RingHomInvPair.ids AddMonoid.nat_smulCommClass

---

← Back to Index