Matrix.UpperTriangularGroup.semidirEquiv_mul_formula |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 484 |
|
Matrix.UpperTriangularGroup.semidirMap |
def |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 451 |
|
Matrix.UpperTriangularGroup.diagonal_map |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 174 |
|
Matrix.UpperTriangularGroup.semidirEquiv_map |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 460 |
|
Matrix.UpperTriangularGroup.semidirEquiv_symm_map |
theorem |
AlgebraicGroups/GroupTheory/UpperTriangular.lean, line 467 |
|
UpperTriangularCoordinateRing.CoordinateRing |
abbrev |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 56 |
|
UpperTriangularCoordinateRing.ideal |
def |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 52 |
|
UpperTriangularCoordinateRing.quotient |
def |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 59 |
|
UpperTriangularCoordinateRing.quotient_lower |
theorem |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 74 |
|
UpperTriangularCoordinateRing.universal |
def |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 79 |
|
UpperTriangularCoordinateRing.universal_detInverse |
theorem |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 95 |
|
UpperTriangularCoordinateRing.ideal_isHopfIdeal |
instance |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 184 |
|
UpperTriangularCoordinateRing.finiteType |
instance |
AlgebraicGroups/Algebra/UpperTriangularCoordinateRing.lean, line 187 |
|
AlgebraicGeometry.upperTriangularGroupScheme |
abbrev |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 66 |
|
AlgebraicGeometry.upperTriangularInclusion |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 76 |
|
AlgebraicGeometry.upperTriangularInclusion_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 88 |
|
AlgebraicGeometry.upperTriangularToGL |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 96 |
|
AlgebraicGeometry.upperTriangularFromGL |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 108 |
|
AlgebraicGeometry.upperTriangularGroupMulEquivAlgHom |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 146 |
|
AlgebraicGeometry.upperTriangularGroupMulEquivPoints |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 189 |
|
AlgebraicGeometry.upperTriangularInclusion_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 202 |
|
AlgebraicGeometry.upperTriangularToGL_natural |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 217 |
|
AlgebraicGeometry.upperTriangularFromGL_natural |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 226 |
|
AlgebraicGeometry.upperTriangularGroupPointsIso |
def |
AlgebraicGroups/GroupScheme/UpperTriangular.lean, line 260 |
|
AlgebraicGeometry.diagonalGroupProjectionCoordinateMap |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 57 |
|
AlgebraicGeometry.diagonalGroupProjectionBialgHom |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 108 |
|
AlgebraicGeometry.diagonalGroupProjection |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 125 |
|
AlgebraicGeometry.diagonalGroupProjection_point |
theorem |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 136 |
|
AlgebraicGeometry.diagonalGroupHomUnits |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 184 |
|
AlgebraicGeometry.multiplicativeGroupHomUnits |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 194 |
|
AlgebraicGeometry.diagonalGroupProjection_globalUnit |
theorem |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 264 |
|
AlgebraicGeometry.diagonalGroupProductFan_forget_isLimit |
abbrev |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 332 |
|
AlgebraicGeometry.diagonalGroupProductFan_isLimit |
abbrev |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 341 |
|
AlgebraicGeometry.diagonalGroupSchemeProductIso |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 347 |
|
AlgebraicGeometry.diagonalGroupSchemeProductIso_hom_π |
theorem |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 352 |
|
AlgebraicGeometry.diagonalGroupSchemeProductIso_inv_projection |
theorem |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 359 |
|
AlgebraicGeometry.diagonalGroupSchemeEmptyIsTerminal |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 366 |
|
AlgebraicGeometry.diagonalGroupSchemeFin0IsTerminal |
def |
AlgebraicGroups/GroupScheme/DiagonalProduct.lean, line 373 |
|
AlgebraicGeometry.upperTriangularDiagonalCoordinateMap |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 54 |
|
AlgebraicGeometry.upperTriangularDiagonalSectionCoordinateMap |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 61 |
|
AlgebraicGeometry.upperTriangularUnitriangularCoordinateMap |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 69 |
|
AlgebraicGeometry.upperTriangularDiagonalProjection |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 286 |
|
AlgebraicGeometry.upperTriangularDiagonalSection |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 292 |
|
AlgebraicGeometry.unitriangularToUpperTriangular |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 298 |
|
AlgebraicGeometry.upperTriangularDiagonal_section |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 349 |
|
AlgebraicGeometry.unitriangularToUpperTriangular_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 317 |
|
AlgebraicGeometry.unitriangularToUpperTriangular_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 370 |
|
AlgebraicGeometry.upperTriangularDiagonalSection_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 390 |
|
AlgebraicGeometry.upperTriangularDiagonalSquare_isPushout |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 469 |
|
AlgebraicGeometry.upperTriangularDiagonalSquare_isPullback |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 563 |
|
AlgebraicGeometry.upperTriangularDiagonalSquare_isPullback_over |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 581 |
|
AlgebraicGeometry.upperTriangularDiagonalSquare_isPullback_group |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 607 |
|
AlgebraicGeometry.upperTriangularDiagonalProjection_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 722 |
|
AlgebraicGeometry.upperTriangularDiagonalSection_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 742 |
|
AlgebraicGeometry.unitriangularToUpperTriangular_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSplitKernel.lean, line 762 |
|
AlgebraicGeometry.upperTriangularSection_over |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 48 |
|
AlgebraicGeometry.upperTriangularDiagonalConj |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 57 |
|
AlgebraicGeometry.upperTriangularDiagonalConj_lift_comp_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 68 |
|
AlgebraicGeometry.upperTriangularSectionFirstIso |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 84 |
|
AlgebraicGeometry.upperTriangularCoordinateChange |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 127 |
|
AlgebraicGeometry.upperTriangularUFirstIso |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 154 |
|
AlgebraicGeometry.upperTriangularUFirstIso_hom |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 161 |
|
AlgebraicGeometry.upperTriangularUFirstIso_hom_comp_diagonal |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 183 |
|
AlgebraicGeometry.upperTriangularUFirstIso_inv_comp_snd |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 203 |
|
AlgebraicGeometry.upperTriangularUFirstIso_inv_fst_comp_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 234 |
|
AlgebraicGeometry.upperTriangularUFirstIso_mul_lift |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 264 |
|
AlgebraicGeometry.upperTriangularUFirstTwistedMul |
def |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 279 |
|
AlgebraicGeometry.upperTriangularUFirstTwistedMul_comp_hom |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 301 |
|
AlgebraicGeometry.upperTriangularDiagonalConj_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 325 |
|
AlgebraicGeometry.upperTriangularUFirstIso_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 361 |
|
AlgebraicGeometry.upperTriangularUFirstIso_inv_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 379 |
|
AlgebraicGeometry.upperTriangularUFirstIso_inv_fst_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 406 |
|
AlgebraicGeometry.upperTriangularUFirstIso_inv_snd_point |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularSchemeProduct.lean, line 417 |
|
AlgebraicGeometry.multiplicativeGroupUnderlyingScheme_smooth |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 87 |
|
AlgebraicGeometry.multiplicativeGroupUnderlyingScheme_geometricallyIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 105 |
|
AlgebraicGeometry.multiplicativeGroupUnderlyingScheme_isIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 331 |
|
AlgebraicGeometry.diagonalGroupUnderlyingScheme_smooth |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 270 |
|
AlgebraicGeometry.diagonalGroupUnderlyingScheme_geometricallyIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 280 |
|
AlgebraicGeometry.diagonalGroupUnderlyingScheme_isIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 336 |
|
AlgebraicGeometry.upperTriangularGroupUnderlyingScheme_smooth |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 305 |
|
AlgebraicGeometry.upperTriangularGroupUnderlyingScheme_geometricallyIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 316 |
|
AlgebraicGeometry.upperTriangularGroupUnderlyingScheme_isIntegral |
instance |
AlgebraicGroups/GroupScheme/FiniteTriangularGeometry.lean, line 344 |
|
Matrix.upperTriangularIndicesEquiv |
def |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 46 |
|
Matrix.upperTriangularIndicesEquiv_diagonal |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 63 |
|
Matrix.upperTriangularIndicesEquiv_strict |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 68 |
|
Matrix.upperTriangularIndicesEquiv_symm_inl |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 73 |
|
Matrix.upperTriangularIndicesEquiv_symm_inr |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 78 |
|
Matrix.upperTriangularIndicesEquiv_coordinates |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 84 |
|
Matrix.upperTriangularRetainedEquiv |
def |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 92 |
|
Matrix.upperTriangularRetainedEquiv_val |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 97 |
|
Matrix.upperTriangularRetainedEquiv_symm_val |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 102 |
|
Matrix.upperTriangularRetainedIndicesEquiv |
def |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 109 |
|
Matrix.upperTriangularRetainedIndicesEquiv_symm_inl_val |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 114 |
|
Matrix.upperTriangularRetainedIndicesEquiv_symm_inr_val |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 119 |
|
Matrix.card_upperTriangularIndices |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 128 |
|
Matrix.card_upperTriangularRetainedIndices |
theorem |
AlgebraicGroups/LinearAlgebra/Matrix/UpperTriangularIndices.lean, line 138 |
|
UpperTriangularCoordinateRing.retainedIndices |
def |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 54 |
|
UpperTriangularCoordinateRing.ideal_eq_localizedCoordinateIdeal |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 59 |
|
UpperTriangularCoordinateRing.localizedPolynomialEquiv |
def |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 83 |
|
UpperTriangularCoordinateRing.localizedPolynomialEquiv_entry |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 92 |
|