UpperTriangularCoordinateRing.localizedPolynomialEquiv_symm_entry |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 119 |
|
UpperTriangularCoordinateRing.erasedDeterminant_eval_one |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 132 |
|
AlgebraicGeometry.upperTriangularCoordinateRing_ringKrullDim |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 180 |
|
AlgebraicGeometry.upperTriangularGroupUnderlyingScheme_topologicalKrullDim |
theorem |
AlgebraicGroups/GroupScheme/UpperTriangularDimension.lean, line 209 |
|
UnitriangularCoordinateRing.comul_entry |
theorem |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 76 |
|
UnitriangularCoordinateRing.baseChange_counit |
theorem |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 91 |
|
UnitriangularCoordinateRing.baseChange_comul |
theorem |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 115 |
|
UnitriangularCoordinateRing.baseChangeBialgEquiv |
def |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 152 |
|
UnitriangularCoordinateRing.baseChangeBialgEquiv_apply |
theorem |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 175 |
|
UnitriangularCoordinateRing.baseChange_antipode |
theorem |
AlgebraicGroups/Algebra/UnitriangularHopfBaseChange.lean, line 187 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularBaseChange.lean, line 71 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeIso_hom_left |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChange.lean, line 96 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeIso_hom_over |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChange.lean, line 104 |
|
AlgebraicGeometry.unitriangularBaseMap |
abbrev |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 62 |
|
AlgebraicGeometry.unitriangularBaseMap_comp |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 66 |
|
AlgebraicGeometry.unitriangularBaseMap_self |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 73 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeTowerIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 79 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeSelfIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 95 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeIso_self |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 527 |
|
AlgebraicGeometry.unitriangularGroupSchemeBaseChangeIso_tower |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularBaseChangeCoherence.lean, line 566 |
|
Subcoalgebra |
structure |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra.lean, line 42 |
|
Subcoalgebra.mk' |
def |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra.lean, line 134 |
|
Subcoalgebra.coalgebra |
def |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Coalgebra.lean, line 197 |
|
Subcoalgebra.subtype |
def |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Hom.lean, line 100 |
|
CoalgHom.codRestrict |
def |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Hom.lean, line 145 |
|
CoalgHom.existsUnique_subtype_comp_iff |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Hom.lean, line 220 |
|
Coalgebra.exists_finite_subcoalgebra |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Finite.lean, line 61 |
|
Coalgebra.exists_finite_subcoalgebra_of_finite |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Subcoalgebra/Finite.lean, line 75 |
|