ZPow

📁 Source: Mathlib/LinearAlgebra/Matrix/ZPow.lean

Statistics

Metric	Count
Definitions instDivInvMonoid, ZPow	2
Theorems det_zpow, mul_zpow, self_zpow, zpow_left, zpow_right, zpow_self, zpow_zpow, zpow_zpow_self, zpow, zpow_right, coe_units_zpow, conjTranspose_zpow, inv_pow', inv_zpow, inv_zpow', isUnit_det_zpow_iff, one_div_pow, one_div_zpow, one_zpow, pow_inv_comm', pow_sub', transpose_zpow, zero_zpow, zero_zpow_eq, zpow_add, zpow_add_of_nonneg, zpow_add_of_nonpos, zpow_add_one, zpow_add_one_of_ne_neg_one, zpow_mul, zpow_mul', zpow_ne_zero_of_isUnit_det, zpow_neg, zpow_neg_mul_zpow_self, zpow_neg_natCast, zpow_neg_one, zpow_one_add, zpow_sub, zpow_sub_one	39
Total	41

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_zpow 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det	Matrix DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	Matrix.det.congr_simp zpow_natCast Matrix.det_pow pow zpow_negSucc Matrix.det_nonsing_inv

Matrix

Definitions

Name	Category	Theorems
instDivInvMonoid 📖	CompOp	38 math math: IsHermitian.zpow, Commute.zpow_self, one_div_pow, isUnit_det_zpow_iff, SemiconjBy.zpow_right, zpow_neg_one, zpow_add, zpow_add_of_nonneg, Commute.mul_zpow, one_zpow, exp_zsmul, Commute.zpow_zpow, IsSymm.zpow, IsUnit.det_zpow, Commute.zpow_zpow_self, Commute.zpow_right, transpose_zpow, zpow_add_of_nonpos, zpow_add_one, conjTranspose_zpow, Commute.self_zpow, Commute.zpow_left, PosSemidef.zpow, zpow_mul', zpow_neg, inv_zpow', zero_zpow_eq, zpow_sub_one, inv_zpow, zpow_one_add, zpow_mul, zpow_neg_natCast, zero_zpow, zpow_neg_mul_zpow_self, zpow_sub, zpow_add_one_of_ne_neg_one, coe_units_zpow, one_div_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_units_zpow 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring Units DivInvMonoid.toZPow Units.instDivInvMonoid instDivInvMonoid	—	zpow_natCast Units.val_pow_eq_pow_val zpow_negSucc inv_pow inv_pow' coe_units_inv
conjTranspose_zpow 📖	mathematical	—	conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing StarRing.toStarAddMonoid Matrix DivInvMonoid.toZPow instDivInvMonoid	—	zpow_natCast conjTranspose_pow zpow_negSucc conjTranspose_nonsing_inv
inv_pow' 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	pow_zero inv_one pow_succ mul_inv_rev pow_succ'
inv_zpow 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid inv	—	zpow_natCast inv_pow' zpow_negSucc
inv_zpow' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid inv	—	zpow_neg inv_zpow
isUnit_det_zpow_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det Matrix DivInvMonoid.toZPow instDivInvMonoid	—	Int.induction_on det.congr_simp zpow_zero det_one zpow_natCast det_pow isUnit_pow_succ_iff neg_add' zpow_neg_natCast isUnit_nonsing_inv_det_iff neg_eq_zero
one_div_pow 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toDiv instDivInvMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	one_div inv_pow'
one_div_zpow 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid DivInvMonoid.toDiv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	one_div inv_zpow
one_zpow 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	zpow_natCast one_pow zpow_negSucc inv_one
pow_inv_comm' 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	inv_pow' pow_zero mul_one one_mul nonsing_inv_cancel_or_zero pow_succ pow_succ' mul_assoc mul_one zero_pow MulZeroClass.zero_mul MulZeroClass.mul_zero
pow_sub' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix Monoid.toNatPow semiring instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub pow_add mul_assoc mul_nonsing_inv det_pow IsUnit.pow mul_one
transpose_zpow 📖	mathematical	—	transpose Matrix DivInvMonoid.toZPow instDivInvMonoid	—	zpow_natCast transpose_pow zpow_negSucc transpose_nonsing_inv
zero_zpow 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	zpow_natCast zero_pow Nat.cast_zero Int.instCharZero zpow_negSucc inv_zero
zero_zpow_eq 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	zpow_zero zero_zpow
zpow_add 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	Int.induction_on add_zero zpow_zero mul_one zpow_add_one mul_assoc zpow_sub_one add_sub_assoc
zpow_add_of_nonneg 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	zpow_natCast pow_add
zpow_add_of_nonpos 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	nonsing_inv_cancel_or_zero zpow_add isUnit_det_of_left_inverse zpow_neg_natCast pow_add
zpow_add_one 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	zpow_natCast pow_succ neg_add neg_add_cancel_right zpow_neg mul_inv_rev mul_assoc nonsing_inv_mul mul_one pow_succ'
zpow_add_one_of_ne_neg_one 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	zpow_natCast pow_succ nonsing_inv_cancel_or_zero zpow_add_one isUnit_det_of_left_inverse zpow_neg_natCast zero_pow MulZeroClass.zero_mul
zpow_mul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid	—	zpow_natCast pow_mul zpow_negSucc zpow_neg_natCast inv_pow' nonsing_inv_nonsing_inv det_pow IsUnit.pow
zpow_mul' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid	—	mul_comm zpow_mul
zpow_ne_zero_of_isUnit_det 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	—	IsUnit.det_zpow Mathlib.Tactic.Contrapose.contrapose₃ det_zero not_isUnit_zero
zpow_neg 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid inv	—	zpow_neg_natCast zpow_negSucc zpow_natCast nonsing_inv_nonsing_inv det_pow IsUnit.pow
zpow_neg_mul_zpow_self 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid DivInvMonoid.toZPow instDivInvMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	zpow_neg nonsing_inv_mul IsUnit.det_zpow
zpow_neg_natCast 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid inv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero zpow_zero pow_zero inv_one DivInvMonoid.zpow_neg'
zpow_neg_one 📖	mathematical	—	Matrix DivInvMonoid.toZPow instDivInvMonoid inv	—	zero_add zpow_one DivInvMonoid.zpow_neg'
zpow_one_add 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	zpow_add zpow_one
zpow_sub 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid DivInvMonoid.toDiv	—	sub_eq_add_neg zpow_add zpow_neg div_eq_mul_inv
zpow_sub_one 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix DivInvMonoid.toZPow instDivInvMonoid instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_assoc mul_nonsing_inv mul_one zpow_add_one sub_add_cancel

Matrix.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_zpow 📖	mathematical	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	DivInvMonoid.toZPow Matrix.instDivInvMonoid Matrix.instHMulOfFintypeOfMulOfAddCommMonoid	—	zpow_natCast Commute.mul_pow zpow_negSucc Matrix.mul_inv_rev Commute.eq Commute.pow_pow
self_zpow 📖	mathematical	—	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	zpow_right Commute.refl
zpow_left 📖	mathematical	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	Commute.symm zpow_right
zpow_right 📖	mathematical	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	Matrix.nonsing_inv_cancel_or_zero Matrix.SemiconjBy.zpow_right Matrix.isUnit_det_of_left_inverse zpow_natCast Commute.pow_right zpow_negSucc zero_pow
zpow_self 📖	mathematical	—	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	zpow_left Commute.refl
zpow_zpow 📖	mathematical	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	zpow_right zpow_left
zpow_zpow_self 📖	mathematical	—	Commute Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	zpow_zpow Commute.refl

Matrix.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zpow 📖	mathematical	Matrix.IsSymm	Matrix DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	eq_1 Matrix.transpose_zpow

Matrix.SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zpow_right 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det SemiconjBy Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	DivInvMonoid.toZPow Matrix.instDivInvMonoid	—	zpow_natCast SemiconjBy.pow_right Matrix.det_pow IsUnit.pow zpow_negSucc Matrix.nonsing_inv_apply SemiconjBy.eq_1 IsRegular.left Matrix.isRegular_of_isLeftRegular_det IsUnit.isRegular mul_assoc SemiconjBy.eq Matrix.mul_smul Algebra.to_smulCommClass Matrix.mul_adjugate Matrix.mul_assoc smul_smul IsUnit.val_inv_mul one_smul Matrix.mul_one Matrix.one_mul

Set

Definitions

Name	Category	Theorems
ZPow 📖	CompOp	5 math math: Nonempty.zpow, singleton_zpow, zpow_eq_empty, Finset.coe_zpow, empty_zpow

---

← Back to Index