Theorems · Definition · ring theory
BialgEquiv.noConfusion
{P : Sort u_1} →
{R : Type u} →
{inst : CommSemiring R} →
{A : Type v} →
{B : Type w} →
{inst_1 : Semiring A} →
{inst_2 : Semiring B} →
{inst_3 : Algebra R A} →
{inst_4 : Algebra R B} →
{inst_5 : CoalgebraStruct R A} →
{inst_6 : CoalgebraStruct R B} →
{t : A ≃ₐc[R] B} →
{R' : Type u} →
{inst' : CommSemiring R'} →
{A' : Type v} →
{B' : Type w} →
{inst'_1 : Semiring A'} →
{inst'_2 : Semiring B'} →
{inst'_3 : Algebra R' A'} →
{inst'_4 : Algebra R' B'} →
{inst'_5 : CoalgebraStruct R' A'} →
{inst'_6 : CoalgebraStruct R' B'} →
{t' : A' ≃ₐc[R'] B'} →
R = R' →
inst ≍ inst' →
A = A' →
B = B' →
inst_1 ≍ inst'_1 →
inst_2 ≍ inst'_2 →
inst_3 ≍ inst'_3 →
inst_4 ≍ inst'_4 →
inst_5 ≍ inst'_5 →
inst_6 ≍ inst'_6 →
t ≍ t' → BialgEquiv.noConfusionType P t t'- Defined in
- Mathlib.RingTheory.Bialgebra.Equiv
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- CoalgebraStructstatement and proof · cited by 230
- AddHom.toFunproof · cited by 168
- LinearMap.toAddHomproof · cited by 165
- BialgEquivstatement and proof · cited by 88
- CoalgEquivproof · cited by 77
- CoalgHom.toLinearMapproof · cited by 36
- CoalgEquiv.toCoalgHomproof · cited by 11
- BialgEquiv.noConfusionTypestatement · cited by 0
- BialgEquiv.casesOnproof · cited by 0
Cited by1
Results whose statement or proof uses this declaration.
- BialgEquiv.mk.noConfusionproof · cited by 1