FinTwo

📁 Source: Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

Statistics

Metric	Count
Definitions IsElliptic, IsHyperbolic, IsParabolic, fixpointPolynomial, upperRightHom, IsElliptic, IsHyperbolic, IsParabolic, parabolicEigenvalue	9
Theorems pow, fixpointPolynomial_eq_zero_iff, injective_upperRightHom, isParabolic_conj_iff, isParabolic_conj_iff', isParabolic_iff_of_upperTriangular, isParabolic_iff_of_upperTriangular_of_det, parabolicEigenvalue_ne_zero, upperRightHom_apply, sub_eigenvalue_sq_eq_zero, disc_conj, disc_conj', discr_conj, discr_conj', isElliptic_conj'_iff, isElliptic_conj_iff, isHyperbolic_conj'_iff, isHyperbolic_conj_iff, isParabolic_conj'_iff, isParabolic_conj_iff, isParabolic_iff_exists, isParabolic_iff_of_upperTriangular, sub_scalar_sq_eq_disc, sub_scalar_sq_eq_discr	24
Total	33

Matrix

Definitions

Name	Category	Theorems
IsElliptic 📖	MathDef	2 math math: isElliptic_conj'_iff, isElliptic_conj_iff
IsHyperbolic 📖	MathDef	2 math math: isHyperbolic_conj_iff, isHyperbolic_conj'_iff
IsParabolic 📖	MathDef	4 math math: isParabolic_iff_of_upperTriangular, isParabolic_iff_exists, isParabolic_conj'_iff, isParabolic_conj_iff
parabolicEigenvalue 📖	CompOp	1 math math: IsParabolic.sub_eigenvalue_sq_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disc_conj 📖	mathematical	—	discr Fin.fintype Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	discr_conj
disc_conj' 📖	mathematical	—	discr Fin.fintype Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	discr_conj'
discr_conj 📖	mathematical	—	discr Fin.fintype Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	Nat.instAtLeastTwoHAddOfNat discr.congr_simp discr_fin_two trace_units_conj det_units_conj
discr_conj' 📖	mathematical	—	discr Fin.fintype Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	discr.congr_simp coe_units_inv inv_inv_of_invertible discr_conj
isElliptic_conj'_iff 📖	mathematical	—	IsElliptic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	coe_units_inv inv_inv_of_invertible isElliptic_conj_iff
isElliptic_conj_iff 📖	mathematical	—	IsElliptic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	discr_conj
isHyperbolic_conj'_iff 📖	mathematical	—	IsHyperbolic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	coe_units_inv inv_inv_of_invertible isHyperbolic_conj_iff
isHyperbolic_conj_iff 📖	mathematical	—	IsHyperbolic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	discr_conj
isParabolic_conj'_iff 📖	mathematical	—	IsParabolic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	coe_units_inv inv_inv_of_invertible isParabolic_conj_iff
isParabolic_conj_iff 📖	mathematical	—	IsParabolic Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	discr_conj smul_eq_mul_diagonal
isParabolic_iff_exists 📖	mathematical	—	IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield nonAssocSemiring Fin.fintype RingHom.instFunLike scalar Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instAtLeastTwoHAddOfNat add_sub_cancel sub_ne_zero IsParabolic.sub_eigenvalue_sq_eq_zero sub_eq_iff_eq_add' RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass MonoidWithZeroHomClass.toMonoidHomClass isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain sub_scalar_sq_eq_discr trace_add scalar_apply trace_diagonal Finset.sum_const Fintype.card_fin nsmul_eq_mul IsNilpotent.eq_zero isNilpotent_trace_of_isNilpotent add_zero mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass add_sub_cancel_left Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Nat.instCharZero div_eq_zero_iff
isParabolic_iff_of_upperTriangular 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsParabolic	—	IsParabolic.eq_1 pow_eq_zero_iff two_ne_zero sub_eq_zero diagonal_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 ext Fintype.complete diagonal_apply_eq
sub_scalar_sq_eq_disc 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fin.fintype sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar DivInvMonoid.toDiv DivisionRing.toDivInvMonoid trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat discr	—	sub_scalar_sq_eq_discr
sub_scalar_sq_eq_discr 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fin.fintype sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar DivInvMonoid.toDiv DivisionRing.toDivInvMonoid trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat discr	—	Nat.instAtLeastTwoHAddOfNat trace_fin_two sq discr_fin_two Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_mul det_fin_two ext Fintype.complete Finset.sum_congr Fin.sum_univ_two diagonal_apply_eq diagonal_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 sub_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero

Matrix.GeneralLinearGroup

Definitions

Name	Category	Theorems
IsElliptic 📖	MathDef	—
IsHyperbolic 📖	MathDef	—
IsParabolic 📖	MathDef	5 math math: Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular, isParabolic_conj_iff, isParabolic_iff_of_upperTriangular, isParabolic_iff_of_upperTriangular_of_det, isParabolic_conj_iff'
fixpointPolynomial 📖	CompOp	2 math math: fixpointPolynomial_eq_zero_iff, fixpointPolynomial_aeval_eq_zero_iff
upperRightHom 📖	CompOp	6 math math: Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular, upperRightHom_apply, isParabolic_iff_of_upperTriangular_of_det, continuous_upperRightHom, Subgroup.mem_strictPeriods_iff, injective_upperRightHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixpointPolynomial_eq_zero_iff 📖	mathematical	—	fixpointPolynomial Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero Matrix Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring Matrix.nonAssocSemiring Fin.fintype RingHom.instFunLike Matrix.scalar Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	fixpointPolynomial.eq_1 map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.coeff_sub Polynomial.coeff_add Polynomial.mul_coeff_zero Polynomial.coeff_C_zero Polynomial.coeff_X_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero Polynomial.coeff_X_zero add_zero zero_sub Polynomial.coeff_C_mul mul_one Polynomial.coeff_mul_X Polynomial.coeff_C_succ sub_self sub_zero zero_add Matrix.ext Fintype.complete Matrix.diagonal_apply_eq Matrix.diagonal_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass MulZeroClass.zero_mul
injective_upperRightHom 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring AddChar.instFunLike upperRightHom	—	injective_iff_map_eq_zero AddMonoidHom.instAddMonoidHomClass Matrix.one_fin_two EquivLike.toEmbeddingLike
isParabolic_conj_iff 📖	mathematical	—	IsParabolic Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Units.instInv	—	Matrix.coe_units_inv
isParabolic_conj_iff' 📖	mathematical	—	IsParabolic Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Units.instInv	—	Matrix.coe_units_inv
isParabolic_iff_of_upperTriangular 📖	mathematical	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fin.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	IsParabolic	—	Matrix.isParabolic_iff_of_upperTriangular isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
isParabolic_iff_of_upperTriangular_of_det 📖	mathematical	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike det Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	IsParabolic AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Ring.toSemiring Units.instMonoid AddChar.instFunLike upperRightHom Matrix.nonUnitalNonAssocRing	—	isParabolic_iff_of_upperTriangular val_det_apply Matrix.det_fin_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left LT.lt.ne' LT.lt.trans_le neg_one_lt_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Matrix.eta_fin_two Matrix.cons_val' Matrix.cons_val_fin_one Iff.not neg_eq_zero neg_neg Matrix.neg_cons Matrix.neg_empty neg_zero
parabolicEigenvalue_ne_zero 📖	—	IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—	Nat.instAtLeastTwoHAddOfNat Matrix.discr_fin_two Matrix.parabolicEigenvalue.eq_1 div_ne_zero_iff eq_true_intro two_ne_zero' sq_eq_zero_iff isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 mul_eq_zero det_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing
upperRightHom_apply 📖	mathematical	—	DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring AddChar.instFunLike upperRightHom Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons AddMonoidWithOne.toOne Matrix.vecEmpty MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—

Matrix.GeneralLinearGroup.IsParabolic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow 📖	mathematical	Matrix.GeneralLinearGroup.IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Monoid.toNatPow Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	—	eq_1 Matrix.isParabolic_iff_exists CharZero.NeZero.two Units.val_pow_eq_pow_val Nat.le_induction pow_one Nat.cast_one tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one one_smul pow_succ mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass add_assoc Matrix.smul_mul IsScalarTower.right smul_zero add_zero Nat.cast_add_one one_mul Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.RingNF.mul_assoc_rev Matrix.GeneralLinearGroup.det_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing zero_add map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Matrix.det_zero IsDomain.to_noZeroDivisors instIsDomain isReduced_of_noZeroDivisors smul_pow Algebra.to_smulCommClass

Matrix.IsParabolic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sub_eigenvalue_sq_eq_zero 📖	mathematical	Matrix.IsParabolic EuclideanDomain.toCommRing Field.toEuclideanDomain	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fin.fintype Matrix.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Matrix.parabolicEigenvalue Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat Matrix.sub_scalar_sq_eq_discr zero_div map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index