Complex

📁 Source: Mathlib/RingTheory/Complex.lean

Statistics

Metric	Count
Definitions	0
Theorems leftMulMatrix_complex, norm_complex_apply, norm_complex_eq, trace_complex_apply	4
Total	4

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftMulMatrix_complex 📖	mathematical	—	DFunLike.coe AlgHom Real Complex Matrix Real.instCommSemiring Complex.instSemiring Matrix.semiring CommSemiring.toSemiring Fin.fintype Complex.instAlgebraOfReal id Matrix.instAlgebra AlgHom.funLike leftMulMatrix Complex.basisOneI Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Complex.re Real.instNeg Complex.im Matrix.vecEmpty	—	Matrix.ext RingHomInvPair.ids leftMulMatrix_eq_repr_mul Complex.coe_basisOneI_repr Complex.coe_basisOneI Complex.mul_re Complex.mul_im Matrix.of_apply Fintype.complete mul_one MulZeroClass.mul_zero sub_zero zero_add zero_sub add_zero
norm_complex_apply 📖	mathematical	—	DFunLike.coe MonoidHom Complex Real MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Complex.instRing CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing MonoidHom.instFunLike norm complexToReal id Complex.instCommSemiring MonoidWithZeroHom Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq	—	norm_eq_matrix_det leftMulMatrix_complex Matrix.det_fin_two Complex.normSq_apply Matrix.cons_val' Matrix.cons_val_fin_one neg_mul sub_neg_eq_add
norm_complex_eq 📖	mathematical	—	norm Real Complex Real.commRing Complex.instRing complexToReal Ring.toSemiring id Complex.instCommSemiring MonoidWithZeroHom.toMonoidHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring Complex.normSq	—	MonoidHom.ext norm_complex_apply
trace_complex_apply 📖	mathematical	—	DFunLike.coe LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Complex.commRing toModule complexToReal id Complex.instCommSemiring Semiring.toModule LinearMap.instFunLike trace Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.re	—	Nat.instAtLeastTwoHAddOfNat trace_eq_matrix_trace leftMulMatrix_complex Matrix.trace_fin_two two_mul

---

← Back to Index