Theorems · Definition · ring theory

Graded.equiv

{E : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_4} →
        {τ : Type u_5} →
          {ι : Type u_6} →
            [inst : SetLike σ A] →
              [inst_1 : SetLike τ B] →
                {𝒜 : ι → σ} →
                  {ℬ : ι → τ} → [inst_2 : EquivLike E A B] → [GradedEquivLike E 𝒜 ℬ] → E → (i : ι) → ↥(𝒜 i) ≃ ↥(ℬ i)

A graded isomorphism descends to an isomorphism on each component.

Defined in

Mathlib.Data.FunLike.Graded

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses Quot.sound

Assumes

SetLikeSetLikeEquivLikeGradedEquivLike