Documentation Verification Report

Equiv

📁 Source: Mathlib/RepresentationTheory/Equiv.lean

Statistics

Metric	Count
Definitions `diagonalOneEquivLeftRegular`, `finsuppTensorLeft`, `finsuppTensorRight`, `freeLift`, `freeLiftLEquiv`, `leftRegularMapEquiv`, `leftRegularTensorTrivialIsoFree`, `ofMulActionSubsingletonEquivTrivial`	8
Theorems `diagonalOneEquivLeftRegular_apply_single`, `diagonalOneEquivLeftRegular_symm_apply_single`, `finsuppTensorLeft_apply_tmul`, `finsuppTensorLeft_apply_tmul_apply`, `finsuppTensorLeft_symm_apply_single`, `finsuppTensorRight_apply_tmul`, `finsuppTensorRight_apply_tmul_apply`, `finsuppTensorRight_symm_apply_single`, `freeLiftLEquiv_apply`, `freeLiftLEquiv_symm_apply`, `freeLift_single_single`, `freeLift_toLinearMap`, `leftRegularMapEquiv_apply`, `leftRegularMapEquiv_symm_apply_toFun`, `leftRegularMapEquiv_symm_single`, `leftRegularTensorTrivialIsoFree_apply_single_tmul_single`, `leftRegularTensorTrivialIsoFree_symm_apply_single_single`, `ofMulActionSubsingletonEquivTrivial_apply`, `ofMulActionSubsingletonEquivTrivial_symm_apply`	19
Total	27

Representation

Definitions

Name	Category	Theorems
`diagonalOneEquivLeftRegular` 📖	CompOp	2 math math: `diagonalOneEquivLeftRegular_symm_apply_single`, `diagonalOneEquivLeftRegular_apply_single`
`finsuppTensorLeft` 📖	CompOp	3 math math: `finsuppTensorLeft_apply_tmul`, `finsuppTensorLeft_symm_apply_single`, `finsuppTensorLeft_apply_tmul_apply`
`finsuppTensorRight` 📖	CompOp	3 math math: `finsuppTensorRight_apply_tmul`, `finsuppTensorRight_symm_apply_single`, `finsuppTensorRight_apply_tmul_apply`
`freeLift` 📖	CompOp	3 math math: `freeLift_single_single`, `freeLift_toLinearMap`, `freeLiftLEquiv_symm_apply`
`freeLiftLEquiv` 📖	CompOp	2 math math: `freeLiftLEquiv_symm_apply`, `freeLiftLEquiv_apply`
`leftRegularMapEquiv` 📖	CompOp	3 math math: `leftRegularMapEquiv_symm_single`, `leftRegularMapEquiv_apply`, `leftRegularMapEquiv_symm_apply_toFun`
`leftRegularTensorTrivialIsoFree` 📖	CompOp	2 math math: `leftRegularTensorTrivialIsoFree_symm_apply_single_single`, `leftRegularTensorTrivialIsoFree_apply_single_tmul_single`
`ofMulActionSubsingletonEquivTrivial` 📖	CompOp	2 math math: `ofMulActionSubsingletonEquivTrivial_symm_apply`, `ofMulActionSubsingletonEquivTrivial_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonalOneEquivLeftRegular_apply_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `diagonal` `leftRegular` `EquivLike.toFunLike` `Equiv.instEquivLike` `diagonalOneEquivLeftRegular` `Finsupp.single`	—	`Finsupp.equivMapDomain_single`
`diagonalOneEquivLeftRegular_symm_apply_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `leftRegular` `diagonal` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `diagonalOneEquivLeftRegular` `Finsupp.single` `uniqueElim` `Fin.instUnique`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearEquiv.isIntertwining_symm_isIntertwining` `Finsupp.domLCongr_symm` `Finsupp.equivMapDomain_single`
`finsuppTensorLeft_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TensorProduct` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `tprod` `finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppTensorLeft` `TensorProduct.tmul` `Finsupp.sum` `instZeroTensorProduct` `Finsupp.single`	—	`TensorProduct.finsuppLeft_apply_tmul`
`finsuppTensorLeft_apply_tmul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.addCommMonoid` `Finsupp.instFunLike` `Equiv` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.instModule` `tprod` `finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppTensorLeft` `TensorProduct.tmul`	—	`finsuppTensorLeft_apply_tmul` `Finsupp.sum_apply` `Finsupp.single_apply` `Finsupp.sum_ite_eq'` `TensorProduct.zero_tmul`
`finsuppTensorLeft_symm_apply_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.addCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.instModule` `finsupp` `tprod` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finsuppTensorLeft` `Finsupp.single` `TensorProduct.tmul`	—	`TensorProduct.finsuppLeft_symm_apply_single`
`finsuppTensorRight_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TensorProduct` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `tprod` `finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppTensorRight` `TensorProduct.tmul` `Finsupp.sum` `instZeroTensorProduct` `Finsupp.single`	—	`TensorProduct.finsuppRight_apply_tmul`
`finsuppTensorRight_apply_tmul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.addCommMonoid` `Finsupp.instFunLike` `Equiv` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.instModule` `tprod` `finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppTensorRight` `TensorProduct.tmul`	—	`finsuppTensorRight_apply_tmul` `Finsupp.sum_apply` `Finsupp.single_apply` `Finsupp.sum_ite_eq'` `TensorProduct.tmul_zero`
`finsuppTensorRight_symm_apply_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.addCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `CommSemiring.toSemiring` `TensorProduct.instModule` `finsupp` `tprod` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finsuppTensorRight` `Finsupp.single` `TensorProduct.tmul`	—	`TensorProduct.finsuppRight_symm_apply_single`
`freeLiftLEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instZero` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `free` `IntertwiningMap.instAddCommMonoid` `Pi.addCommMonoid` `IntertwiningMap.instModule` `Pi.Function.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `freeLiftLEquiv` `IntertwiningMap.instFunLike` `Finsupp.single` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids`
`freeLiftLEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instZero` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `free` `Pi.addCommMonoid` `IntertwiningMap.instAddCommMonoid` `Pi.Function.module` `IntertwiningMap.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `freeLiftLEquiv` `freeLift`	—	`RingHomInvPair.ids`
`freeLift_single_single` 📖	mathematical	—	`DFunLike.coe` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instZero` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `free` `IntertwiningMap.instFunLike` `freeLift` `Finsupp.single` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`Finsupp.uncurry_single` `Finsupp.linearCombination_single`
`freeLift_toLinearMap` 📖	mathematical	—	`IntertwiningMap.toLinearMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instZero` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `free` `freeLift` `LinearMap.comp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `RingHom.id` `Finsupp.linearCombination` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `LinearEquiv.toLinearMap` `LinearEquiv.symm` `Finsupp.curryLinearEquiv`	—	—
`leftRegularMapEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `leftRegular` `IntertwiningMap.instAddCommMonoid` `IntertwiningMap.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `leftRegularMapEquiv` `IntertwiningMap.instFunLike` `Finsupp.single` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids`
`leftRegularMapEquiv_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `leftRegular` `IntertwiningMap.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `IntertwiningMap.instAddCommMonoid` `IntertwiningMap.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `leftRegularMapEquiv` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`RingHomInvPair.ids`
`leftRegularMapEquiv_symm_single` 📖	mathematical	—	`DFunLike.coe` `IntertwiningMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `leftRegular` `IntertwiningMap.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `IntertwiningMap.instAddCommMonoid` `IntertwiningMap.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `leftRegularMapEquiv` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `LinearMap` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`RingHomInvPair.ids` `Finsupp.sum_single_index` `zero_smul` `one_smul`
`leftRegularTensorTrivialIsoFree_apply_single_tmul_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TensorProduct` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Finsupp.instZero` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `tprod` `leftRegular` `trivial` `free` `EquivLike.toFunLike` `Equiv.instEquivLike` `leftRegularTensorTrivialIsoFree` `TensorProduct.tmul` `Finsupp.single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`finsuppTensorFinsupp'_single_tmul_single` `Finsupp.equivMapDomain_single` `Finsupp.curry_single`
`leftRegularTensorTrivialIsoFree_symm_apply_single_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instZero` `TensorProduct` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `free` `tprod` `leftRegular` `trivial` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `leftRegularTensorTrivialIsoFree` `Finsupp.single` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearEquiv.isIntertwining_symm_isIntertwining` `LinearEquiv.trans.congr_simp` `Finsupp.domLCongr_symm` `Finsupp.uncurry_single` `Finsupp.equivMapDomain_single` `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul`
`ofMulActionSubsingletonEquivTrivial_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `IntertwiningMap.toLinearMap` `ofMulAction` `trivial` `Equiv.toIntertwiningMap` `ofMulActionSubsingletonEquivTrivial` `Finsupp.instFunLike` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`ofMulActionSubsingletonEquivTrivial_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Semiring.toModule` `Finsupp.module` `LinearMap.instFunLike` `IntertwiningMap.toLinearMap` `trivial` `ofMulAction` `Equiv.toIntertwiningMap` `Equiv.symm` `ofMulActionSubsingletonEquivTrivial` `Finsupp.single` `MulOne.toOne` `MulOneClass.toMulOne`	—	`Finsupp.LinearEquiv.finsuppUnique_symm_apply`

---

← Back to Index