AlgebraicGeometry.unitriangularStageConjugation_point |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageNormality.lean, line 166 |
|
UnitriangularStageCoordinateRing.coordinate_counit |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageCoordinates.lean, line 75 |
|
UnitriangularStageCoordinateRing.coordinate_comul |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageCoordinates.lean, line 95 |
|
UnitriangularStageCoordinateRing.coordinateBialgHom |
def |
AlgebraicGroups/Algebra/UnitriangularStageCoordinates.lean, line 163 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap |
def |
AlgebraicGroups/GroupScheme/UnitriangularStageCoordinates.lean, line 71 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_point |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageCoordinates.lean, line 196 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_point_natural |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageCoordinates.lean, line 214 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_successor_zero |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageCoordinates.lean, line 143 |
|
UnitriangularStageCoordinateRing.coordinateBialgHom_toAlgHom |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageKernel.lean, line 37 |
|
UnitriangularStageCoordinateRing.ideal_succ_eq_sup |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageKernel.lean, line 46 |
|
UnitriangularStageCoordinateRing.existsUnique_comp_successor |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageKernel.lean, line 75 |
|
AlgebraicGeometry.unitriangularStageSuccessor_existsUnique_scheme |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageKernel.lean, line 142 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_isPullback |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageKernel.lean, line 157 |
|
AlgebraicGeometry.unitriangularUnderlyingAffineSpaceIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 63 |
|
AlgebraicGeometry.unitriangularUnderlyingAffineSpaceIso_preimage_variable |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 85 |
|
AlgebraicGeometry.unitriangularUnderlyingAffineSpaceIso_preimage_inverse |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 104 |
|
AlgebraicGeometry.unitriangularCoordinateRing_standardSmooth |
instance |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 124 |
|
AlgebraicGeometry.unitriangularCoordinateRing_finitePresentation |
instance |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 129 |
|
AlgebraicGeometry.unitriangularGroupUnderlyingScheme_smooth |
instance |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 135 |
|
AlgebraicGeometry.unitriangularGroupUnderlyingScheme_geometricallyIntegral |
instance |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 145 |
|
AlgebraicGeometry.unitriangularGroupUnderlyingScheme_isIntegral |
instance |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 162 |
|
AlgebraicGeometry.card_strictUpperPair |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 169 |
|
AlgebraicGeometry.unitriangularCoordinateRing_ringKrullDim |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 181 |
|
AlgebraicGeometry.unitriangularGroupUnderlyingScheme_topologicalKrullDim |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 193 |
|
AlgebraicGeometry.unitriangularGroupUnderlyingScheme_topologicalKrullDim_fin |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularGeometry.lean, line 203 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup |
def |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 135 |
|
Matrix.UnitriangularGroup.mem_superdiagonalSubgroup |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 163 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_one |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 171 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_zero |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 177 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_antitone |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 183 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_succ_le |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 189 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_end |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 194 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_normal |
instance |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 209 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_commutator |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 233 |
|
Matrix.UnitriangularGroup.descendingSeries |
def |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 286 |
|
Matrix.UnitriangularGroup.descendingSeries_isDescendingCentralSeries |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 292 |
|
Matrix.UnitriangularGroup.descendingSeries_end |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 306 |
|
Matrix.UnitriangularGroup.instIsNilpotent |
instance |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 321 |
|
Matrix.UnitriangularGroup.nilpotencyClass_le |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 330 |
|
Matrix.UnitriangularGroup.map_mem_superdiagonalSubgroup |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 343 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_map |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularCentralFiltration.lean, line 354 |
|
Matrix.UnitriangularGroup.superdiagonalIndex |
abbrev |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 41 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateHom |
def |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 82 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateHom_apply |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 98 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateHom_ker |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 107 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateHom_surjective |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 157 |
|
Matrix.UnitriangularGroup.superdiagonalQuotientEquiv |
def |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 197 |
|
Matrix.UnitriangularGroup.superdiagonalQuotientEquiv_mk |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 206 |
|
Matrix.UnitriangularGroup.superdiagonalStageMap |
def |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 217 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateMap |
def |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 225 |
|
Matrix.UnitriangularGroup.superdiagonalCoordinateHom_natural |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 240 |
|
Matrix.UnitriangularGroup.superdiagonalQuotientMap |
def |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 253 |
|
Matrix.UnitriangularGroup.superdiagonalQuotientEquiv_natural |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularSuperdiagonalQuotients.lean, line 267 |
|
Matrix.UnitriangularGroup.elementary |
def |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 41 |
|
Matrix.UnitriangularGroup.elementary_gl |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 53 |
|
Matrix.UnitriangularGroup.elementary_coe |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 58 |
|
Matrix.UnitriangularGroup.elementary_commutator |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 65 |
|
Matrix.UnitriangularGroup.nilpotencyClass_eq_of_nontrivial |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 118 |
|
Matrix.UnitriangularGroup.nilpotencyClass_eq_zero_of_subsingleton |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularNilpotencyClass.lean, line 146 |
|
Matrix.UnitriangularGroup.elementary_mem_lowerCentralSeries_of_distance |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularLowerCentralSeries.lean, line 39 |
|
Matrix.UnitriangularGroup.elementary_mem_superdiagonalSubgroup |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularLowerCentralSeries.lean, line 61 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_le_of_elementary_mem |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularLowerCentralSeries.lean, line 179 |
|
Matrix.UnitriangularGroup.lowerCentralSeries_eq_superdiagonalSubgroup |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularLowerCentralSeries.lean, line 225 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_commutator_eq |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularDerivedSeries.lean, line 40 |
|
Matrix.UnitriangularGroup.derivedSeries_eq_superdiagonalSubgroup |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularDerivedSeries.lean, line 61 |
|
Matrix.UnitriangularGroup.superdiagonalSubgroup_eq_bot_iff |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularDerivedSeries.lean, line 79 |
|
Matrix.UnitriangularGroup.derivedSeries_eq_bot_iff |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularDerivedSeries.lean, line 100 |
|
Matrix.pow_card_eq_zero_of_upperTriangular_diag_zero |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularExponent.lean, line 46 |
|
Matrix.UnitriangularGroup.pow_prime_pow_eq_one |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularExponent.lean, line 110 |
|
Matrix.UnitriangularGroup.exists_pow_ne_one_of_pos_lt |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularExponent.lean, line 138 |
|
Matrix.UnitriangularGroup.forall_pow_prime_pow_eq_one_iff |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularExponent.lean, line 197 |
|
Matrix.UnitriangularGroup.exponent_dvd_prime_pow_iff |
theorem |
AlgebraicGroups/GroupTheory/UnitriangularExponent.lean, line 212 |
|
Matrix.diagonalSubgroup |
def |
AlgebraicGroups/GroupTheory/Diagonal.lean, line 52 |
|
Matrix.DiagonalGroup.unitsEquiv |
def |
AlgebraicGroups/GroupTheory/Diagonal.lean, line 129 |
|
Matrix.DiagonalGroup.map |
def |
AlgebraicGroups/GroupTheory/Diagonal.lean, line 166 |
|
DiagonalCoordinateRing.ideal_isHopfIdeal |
instance |
AlgebraicGroups/Algebra/DiagonalCoordinateRing.lean, line 189 |
|
DiagonalCoordinateRing.universal_detInverse |
theorem |
AlgebraicGroups/Algebra/DiagonalCoordinateRing.lean, line 94 |
|
DiagonalCoordinateRing.finiteType |
instance |
AlgebraicGroups/Algebra/DiagonalCoordinateRing.lean, line 192 |
|
AlgebraicGeometry.diagonalGroupScheme |
abbrev |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 66 |
|
AlgebraicGeometry.diagonalInclusion_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 84 |
|
AlgebraicGeometry.diagonalGroupMulEquivPoints |
def |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 191 |
|
AlgebraicGeometry.diagonalInclusion_point |
theorem |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 203 |
|
AlgebraicGeometry.diagonalGroupPointsIso |
def |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 266 |
|
AlgebraicGeometry.diagonalGroupUnitsEquivPoints |
def |
AlgebraicGroups/GroupScheme/Diagonal.lean, line 289 |
|
MvPolynomial.card_le_card_of_unique_common_zero |
theorem |
AlgebraicGroups/Algebra/AlgebraicallyClosedCommonZero.lean, line 63 |
|
MvPolynomial.exists_common_zero_ne |
theorem |
AlgebraicGroups/Algebra/AlgebraicallyClosedCommonZero.lean, line 95 |
|
MvPolynomial.exists_nonzero_common_zero_of_isHomogeneous |
theorem |
AlgebraicGroups/Algebra/AlgebraicallyClosedCommonZero.lean, line 115 |
|
Matrix.upperTriangularSubgroup |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 54 |
|
Matrix.UpperTriangularGroup.map |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 86 |
|
Matrix.UpperTriangularGroup.isUnit_entry |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 114 |
|
Matrix.UpperTriangularGroup.diagonal |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 122 |
|
Matrix.UpperTriangularGroup.diagonalSection |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 157 |
|
Matrix.UnitriangularGroup.inUpperTriangular |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 192 |
|
Matrix.UpperTriangularGroup.range_unitriangular |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 215 |
|
Matrix.UpperTriangularGroup.kernelEquiv |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 236 |
|
Matrix.UpperTriangularGroup.diagonalAction |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 255 |
|
Matrix.UpperTriangularGroup.diagonalAction_apply |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 388 |
|
Matrix.UpperTriangularGroup.unipotentPart |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 276 |
|
Matrix.UpperTriangularGroup.unipotentPart_apply |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 365 |
|
Matrix.UpperTriangularGroup.semidirEquiv |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 319 |
|