SymplecticGroup

📁 Source: Mathlib/LinearAlgebra/SymplecticGroup.lean

Statistics

Metric	Count
Definitions J, symplecticGroup, coeMatrix, hasInv, instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup, symJ	6
Theorems J_det_mul_J_det, J_inv, J_squared, J_transpose, isUnit_det_J, J_mem, coe_J, coe_inv, coe_inv', inv_eq_symplectic_inv, inv_left_mul_aux, mem_iff, mem_iff', neg_mem, symplectic_det, transpose_mem, transpose_mem_iff	17
Total	23

Matrix

Definitions

Name	Category	Theorems
J 📖	CompOp	12 math math: SymplecticGroup.coe_inv, SymplecticGroup.coe_J, SymplecticGroup.mem_iff, J_squared, J_transpose, isUnit_det_J, SymplecticGroup.mem_iff', SymplecticGroup.inv_left_mul_aux, J_inv, J_det_mul_J_det, SymplecticGroup.J_mem, SymplecticGroup.inv_eq_symplectic_inv
symplecticGroup 📖	CompOp	7 math math: SymplecticGroup.transpose_mem_iff, SymplecticGroup.coe_inv, SymplecticGroup.coe_J, SymplecticGroup.mem_iff, SymplecticGroup.mem_iff', SymplecticGroup.coe_inv', SymplecticGroup.J_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
J_det_mul_J_det 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing det instFintypeSum J AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	det_mul J_squared one_smul smul_neg neg_smul det_smul Fintype.card_sum det_one mul_one Even.neg_one_pow Even.add_self
J_inv 📖	mathematical	—	Matrix inv instFintypeSum J neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	inv_eq_right_inv mul_neg J_squared neg_neg
J_squared 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid J neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	J.eq_1 fromBlocks_multiply zero_mul neg_mul one_mul zero_add neg_zero add_zero fromBlocks_neg fromBlocks_one
J_transpose 📖	mathematical	—	transpose J Matrix neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	J.eq_1 fromBlocks_transpose neg_one_smul fromBlocks_smul transpose_zero transpose_one transpose_neg smul_zero smul_neg neg_smul one_smul neg_neg
isUnit_det_J 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det instFintypeSum J	—	isUnit_iff_exists_inv instIsDedekindFiniteMonoid J_det_mul_J_det

SymplecticGroup

Definitions

Name	Category	Theorems
coeMatrix 📖	CompOp	—
hasInv 📖	CompOp	2 math math: coe_inv, coe_inv'
instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup 📖	CompOp	—
symJ 📖	CompOp	1 math math: coe_J

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
J_mem 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup Matrix.J	—	mem_iff Matrix.J.eq_1 Matrix.fromBlocks_multiply Matrix.fromBlocks_transpose MulZeroClass.mul_zero mul_one zero_add mul_neg neg_zero add_zero Matrix.transpose_neg Matrix.transpose_one neg_neg
coe_J 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup symJ Matrix.J	—	—
coe_inv 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup hasInv Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Matrix.J Matrix.transpose	—	—
coe_inv' 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup hasInv Matrix.inv	—	coe_inv Matrix.inv_eq_left_inv neg_mul inv_left_mul_aux
inv_eq_symplectic_inv 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup	Matrix.inv Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Matrix.J Matrix.transpose	—	Matrix.inv_eq_left_inv Matrix.neg_mul inv_left_mul_aux
inv_left_mul_aux 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup	Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.J Matrix.transpose Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Matrix.mul_assoc Matrix.neg_mul mem_iff' neg_smul one_smul Matrix.J_squared neg_smul_neg
mem_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.J Matrix.transpose	—	—
mem_iff' 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose Matrix.J	—	transpose_mem_iff mem_iff Matrix.transpose_transpose
neg_mem 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup	Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	mem_iff neg_mul Matrix.transpose_neg mul_neg neg_neg
symplectic_det 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.det	—	isUnit_iff_exists_inv instIsDedekindFiniteMonoid IsUnit.mul_left_cancel Matrix.isUnit_det_J mul_one mul_assoc mul_comm Matrix.det_mul Matrix.det_transpose mem_iff
transpose_mem 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup	Matrix.transpose	—	mem_iff Matrix.transpose_transpose symplectic_det Matrix.det_transpose Matrix.J_inv mul_neg neg_mul neg_neg Matrix.mul_assoc Matrix.mul_inv_rev Matrix.neg_mul Matrix.mul_nonsing_inv_cancel_left Matrix.nonsing_inv_mul_cancel_right
transpose_mem_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFintypeSum SetLike.instMembership Submonoid.instSetLike Matrix.symplecticGroup Matrix.transpose	—	Matrix.transpose_transpose transpose_mem

---

← Back to Index