NormTrace

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_one_add_smul` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `norm` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `toSMul` `Distrib.toMul` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `trace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`norm_eq_matrix_det` `trace_eq_matrix_trace` `Matrix.det.congr_simp` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Matrix.det_one_add_smul`

---