PID

Statistics

Metric	Count
Definitions	0
Theorems `trace_restrict_eq_of_forall_mem`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`trace_restrict_eq_of_forall_mem` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`Submodule.addCommMonoid` `Submodule.module` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `trace` `restrict`	—	`smulCommClass_self` `Finite.of_fintype` `RingHomInvPair.ids` `trace_eq_matrix_trace` `Mathlib.Tactic.Contrapose.contrapose₂` `Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range` `Finset.sum_filter_of_ne` `Finset.sum_congr` `Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix` `Finset.filter.congr_simp` `Finset.univ_filter_exists` `Finset.sum_image` `Function.Injective.injOn` `Function.Embedding.injective`

---