TransferInstance

Statistics

Metric	Count
Definitions `addAction`, `mulAction`, `mulDistribMulAction`	3
Theorems `faithfulSMul`, `faithfulVAdd`, `isCentralScalar`, `isCentralVAdd`, `isScalarTower`, `smulCommClass`, `vaddAssocClass`, `vaddCommClass`	8
Total	11

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `smul`	—	`EquivLike.toEmbeddingLike` `forall_congr_right` `FaithfulSMul.eq_of_smul_eq_smul`
`faithfulVAdd` 📖	mathematical	—	`FaithfulVAdd` `vadd`	—	`EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `forall_congr_right` `FaithfulVAdd.eq_of_vadd_eq_vadd`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `smul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `vadd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `smul`	—	`smul_assoc` `apply_symm_apply`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `smul`	—	`apply_symm_apply` `SMulCommClass.smul_comm`
`vaddAssocClass` 📖	mathematical	—	`VAddAssocClass` `vadd`	—	`vadd_assoc` `apply_symm_apply`
`vaddCommClass` 📖	mathematical	—	`VAddCommClass` `vadd`	—	`apply_symm_apply` `VAddCommClass.vadd_comm`

---