Documentation

Mathlib.Logic.Equiv.TransferInstance

Transfer algebraic structures across Equivs #

In this file we prove theorems of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups, rings, integral domains, fields and so on.

Note that most of these constructions can also be obtained using the transport tactic.

Implementation details #

When adding new definitions that transfer type-classes across an equivalence, please use abbrev. See note [reducible non-instances].

Tags #

equiv, group, ring, field, module, algebra

@[reducible, inline]
abbrev Equiv.zero {α : Type u} {β : Type v} (e : α β) [Zero β] :
Zero α

Transfer Zero across an Equiv

Equations
  • e.zero = { zero := e.symm 0 }
Instances For
    @[reducible, inline]
    abbrev Equiv.one {α : Type u} {β : Type v} (e : α β) [One β] :
    One α

    Transfer One across an Equiv

    Equations
    • e.one = { one := e.symm 1 }
    Instances For
      theorem Equiv.zero_def {α : Type u} {β : Type v} (e : α β) [Zero β] :
      0 = e.symm 0
      theorem Equiv.one_def {α : Type u} {β : Type v} (e : α β) [One β] :
      1 = e.symm 1
      noncomputable instance Equiv.instZeroShrink {α : Type u} [Small.{v, u} α] [Zero α] :
      Equations
      noncomputable instance Equiv.instOneShrink {α : Type u} [Small.{v, u} α] [One α] :
      Equations
      @[reducible, inline]
      abbrev Equiv.add {α : Type u} {β : Type v} (e : α β) [Add β] :
      Add α

      Transfer Add across an Equiv

      Equations
      • e.add = { add := fun (x y : α) => e.symm (e x + e y) }
      Instances For
        @[reducible, inline]
        abbrev Equiv.mul {α : Type u} {β : Type v} (e : α β) [Mul β] :
        Mul α

        Transfer Mul across an Equiv

        Equations
        • e.mul = { mul := fun (x y : α) => e.symm (e x * e y) }
        Instances For
          theorem Equiv.add_def {α : Type u} {β : Type v} (e : α β) [Add β] (x : α) (y : α) :
          x + y = e.symm (e x + e y)
          theorem Equiv.mul_def {α : Type u} {β : Type v} (e : α β) [Mul β] (x : α) (y : α) :
          x * y = e.symm (e x * e y)
          noncomputable instance Equiv.instAddShrink {α : Type u} [Small.{v, u} α] [Add α] :
          Equations
          noncomputable instance Equiv.instMulShrink {α : Type u} [Small.{v, u} α] [Mul α] :
          Equations
          @[reducible, inline]
          abbrev Equiv.sub {α : Type u} {β : Type v} (e : α β) [Sub β] :
          Sub α

          Transfer Sub across an Equiv

          Equations
          • e.sub = { sub := fun (x y : α) => e.symm (e x - e y) }
          Instances For
            @[reducible, inline]
            abbrev Equiv.div {α : Type u} {β : Type v} (e : α β) [Div β] :
            Div α

            Transfer Div across an Equiv

            Equations
            • e.div = { div := fun (x y : α) => e.symm (e x / e y) }
            Instances For
              theorem Equiv.sub_def {α : Type u} {β : Type v} (e : α β) [Sub β] (x : α) (y : α) :
              x - y = e.symm (e x - e y)
              theorem Equiv.div_def {α : Type u} {β : Type v} (e : α β) [Div β] (x : α) (y : α) :
              x / y = e.symm (e x / e y)
              noncomputable instance Equiv.instSubShrink {α : Type u} [Small.{v, u} α] [Sub α] :
              Equations
              noncomputable instance Equiv.instDivShrink {α : Type u} [Small.{v, u} α] [Div α] :
              Equations
              @[reducible, inline]
              abbrev Equiv.Neg {α : Type u} {β : Type v} (e : α β) [Neg β] :
              Neg α

              Transfer Neg across an Equiv

              Equations
              • e.Neg = { neg := fun (x : α) => e.symm (-e x) }
              Instances For
                @[reducible, inline]
                abbrev Equiv.Inv {α : Type u} {β : Type v} (e : α β) [Inv β] :
                Inv α

                Transfer Inv across an Equiv

                Equations
                • e.Inv = { inv := fun (x : α) => e.symm (e x)⁻¹ }
                Instances For
                  theorem Equiv.neg_def {α : Type u} {β : Type v} (e : α β) [Neg β] (x : α) :
                  -x = e.symm (-e x)
                  theorem Equiv.inv_def {α : Type u} {β : Type v} (e : α β) [Inv β] (x : α) :
                  x⁻¹ = e.symm (e x)⁻¹
                  noncomputable instance Equiv.instNegShrink {α : Type u} [Small.{v, u} α] [Neg α] :
                  Equations
                  noncomputable instance Equiv.instInvShrink {α : Type u} [Small.{v, u} α] [Inv α] :
                  Equations
                  @[reducible, inline]
                  abbrev Equiv.smul {α : Type u} {β : Type v} (e : α β) (R : Type u_1) [SMul R β] :
                  SMul R α

                  Transfer SMul across an Equiv

                  Equations
                  • e.smul R = { smul := fun (r : R) (x : α) => e.symm (r e x) }
                  Instances For
                    theorem Equiv.smul_def {α : Type u} {β : Type v} (e : α β) {R : Type u_1} [SMul R β] (r : R) (x : α) :
                    r x = e.symm (r e x)
                    noncomputable instance Equiv.instSMulShrink {α : Type u} [Small.{v, u} α] (R : Type u_1) [SMul R α] :
                    Equations
                    @[reducible]
                    def Equiv.pow {α : Type u} {β : Type v} (e : α β) (N : Type u_1) [Pow β N] :
                    Pow α N

                    Transfer Pow across an Equiv

                    Equations
                    • e.pow N = { pow := fun (x : α) (n : N) => e.symm (e x ^ n) }
                    Instances For
                      theorem Equiv.pow_def {α : Type u} {β : Type v} (e : α β) {N : Type u_1} [Pow β N] (n : N) (x : α) :
                      x ^ n = e.symm (e x ^ n)
                      noncomputable instance Equiv.instPowShrink {α : Type u} [Small.{v, u} α] (N : Type u_1) [Pow α N] :
                      Equations
                      theorem Equiv.addEquiv.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [Add β] (x : α) (y : α) :
                      e.toFun (x + y) = e.toFun x + e.toFun y
                      def Equiv.addEquiv {α : Type u} {β : Type v} (e : α β) [Add β] :
                      let mul := e.add; α ≃+ β

                      An equivalence e : α ≃ β gives an additive equivalence α ≃+ β where the additive structure on α is the one obtained by transporting an additive structure on β back along e.

                      Equations
                      • e.addEquiv = { toEquiv := e, map_add' := }
                      Instances For
                        def Equiv.mulEquiv {α : Type u} {β : Type v} (e : α β) [Mul β] :
                        let mul := e.mul; α ≃* β

                        An equivalence e : α ≃ β gives a multiplicative equivalence α ≃* β where the multiplicative structure on α is the one obtained by transporting a multiplicative structure on β back along e.

                        Equations
                        • e.mulEquiv = { toEquiv := e, map_mul' := }
                        Instances For
                          @[simp]
                          theorem Equiv.addEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] (a : α) :
                          e.addEquiv a = e a
                          @[simp]
                          theorem Equiv.mulEquiv_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (a : α) :
                          e.mulEquiv a = e a
                          theorem Equiv.addEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] (b : β) :
                          (AddEquiv.symm e.addEquiv) b = e.symm b
                          theorem Equiv.mulEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (b : β) :
                          (MulEquiv.symm e.mulEquiv) b = e.symm b
                          noncomputable def Shrink.addEquiv {α : Type u} [Small.{v, u} α] [Add α] :

                          Shrink α to a smaller universe preserves addition.

                          Equations
                          Instances For
                            noncomputable def Shrink.mulEquiv {α : Type u} [Small.{v, u} α] [Mul α] :

                            Shrink α to a smaller universe preserves multiplication.

                            Equations
                            Instances For
                              def Equiv.ringEquiv {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] :
                              let add := e.add; let mul := e.mul; α ≃+* β

                              An equivalence e : α ≃ β gives a ring equivalence α ≃+* β where the ring structure on α is the one obtained by transporting a ring structure on β back along e.

                              Equations
                              • e.ringEquiv = { toEquiv := e, map_mul' := , map_add' := }
                              Instances For
                                @[simp]
                                theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (a : α) :
                                e.ringEquiv a = e a
                                theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (b : β) :
                                (RingEquiv.symm e.ringEquiv) b = e.symm b
                                noncomputable def Shrink.ringEquiv (α : Type u) [Small.{v, u} α] [Ring α] :

                                Shrink α to a smaller universe preserves ring structure.

                                Equations
                                Instances For
                                  theorem Equiv.addSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddSemigroup β] :
                                  ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                  @[reducible, inline]
                                  abbrev Equiv.addSemigroup {α : Type u} {β : Type v} (e : α β) [AddSemigroup β] :

                                  Transfer add_semigroup across an Equiv

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Equiv.semigroup {α : Type u} {β : Type v} (e : α β) [Semigroup β] :

                                    Transfer Semigroup across an Equiv

                                    Equations
                                    Instances For
                                      Equations
                                      • Equiv.instAddSemigroupShrink = (equivShrink α).symm.addSemigroup
                                      noncomputable instance Equiv.instSemigroupShrink {α : Type u} [Small.{v, u} α] [Semigroup α] :
                                      Equations
                                      @[reducible, inline]
                                      abbrev Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α β) [SemigroupWithZero β] :

                                      Transfer SemigroupWithZero across an Equiv

                                      Equations
                                      Instances For
                                        Equations
                                        • Equiv.instAddSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero
                                        Equations
                                        • Equiv.instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero
                                        @[reducible, inline]
                                        abbrev Equiv.addCommSemigroup {α : Type u} {β : Type v} (e : α β) [AddCommSemigroup β] :

                                        Transfer AddCommSemigroup across an Equiv

                                        Equations
                                        Instances For
                                          theorem Equiv.addCommSemigroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommSemigroup β] :
                                          ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                          @[reducible, inline]
                                          abbrev Equiv.commSemigroup {α : Type u} {β : Type v} (e : α β) [CommSemigroup β] :

                                          Transfer CommSemigroup across an Equiv

                                          Equations
                                          Instances For
                                            Equations
                                            • Equiv.instAddCommSemigroupShrink = (equivShrink α).symm.addCommSemigroup
                                            Equations
                                            • Equiv.instCommSemigroupShrink = (equivShrink α).symm.commSemigroup
                                            @[reducible, inline]
                                            abbrev Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α β) [MulZeroClass β] :

                                            Transfer MulZeroClass across an Equiv

                                            Equations
                                            Instances For
                                              Equations
                                              • Equiv.instMulZeroClassShrink = (equivShrink α).symm.mulZeroClass
                                              theorem Equiv.addZeroClass.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddZeroClass β] :
                                              ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                              @[reducible, inline]
                                              abbrev Equiv.addZeroClass {α : Type u} {β : Type v} (e : α β) [AddZeroClass β] :

                                              Transfer AddZeroClass across an Equiv

                                              Equations
                                              Instances For
                                                theorem Equiv.addZeroClass.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddZeroClass β] :
                                                e (e.symm 0) = 0
                                                @[reducible, inline]
                                                abbrev Equiv.mulOneClass {α : Type u} {β : Type v} (e : α β) [MulOneClass β] :

                                                Transfer MulOneClass across an Equiv

                                                Equations
                                                Instances For
                                                  Equations
                                                  • Equiv.instAddZeroClassShrink = (equivShrink α).symm.addZeroClass
                                                  noncomputable instance Equiv.instMulOneClassShrink {α : Type u} [Small.{v, u} α] [MulOneClass α] :
                                                  Equations
                                                  • Equiv.instMulOneClassShrink = (equivShrink α).symm.mulOneClass
                                                  @[reducible, inline]
                                                  abbrev Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α β) [MulZeroOneClass β] :

                                                  Transfer MulZeroOneClass across an Equiv

                                                  Equations
                                                  Instances For
                                                    Equations
                                                    • Equiv.instMulZeroOneClassShrink = (equivShrink α).symm.mulZeroOneClass
                                                    @[reducible, inline]
                                                    abbrev Equiv.addMonoid {α : Type u} {β : Type v} (e : α β) [AddMonoid β] :

                                                    Transfer AddMonoid across an Equiv

                                                    Equations
                                                    Instances For
                                                      theorem Equiv.addMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddMonoid β] :
                                                      e (e.symm 0) = 0
                                                      theorem Equiv.addMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddMonoid β] :
                                                      ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                                      theorem Equiv.addMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddMonoid β] :
                                                      ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                      @[reducible, inline]
                                                      abbrev Equiv.monoid {α : Type u} {β : Type v} (e : α β) [Monoid β] :

                                                      Transfer Monoid across an Equiv

                                                      Equations
                                                      Instances For
                                                        noncomputable instance Equiv.instAddMonoidShrink {α : Type u} [Small.{v, u} α] [AddMonoid α] :
                                                        Equations
                                                        noncomputable instance Equiv.instMonoidShrink {α : Type u} [Small.{v, u} α] [Monoid α] :
                                                        Equations
                                                        theorem Equiv.addCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommMonoid β] :
                                                        ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                        theorem Equiv.addCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommMonoid β] :
                                                        e (e.symm 0) = 0
                                                        @[reducible, inline]
                                                        abbrev Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α β) [AddCommMonoid β] :

                                                        Transfer AddCommMonoid across an Equiv

                                                        Equations
                                                        Instances For
                                                          theorem Equiv.addCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommMonoid β] :
                                                          ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                                          @[reducible, inline]
                                                          abbrev Equiv.commMonoid {α : Type u} {β : Type v} (e : α β) [CommMonoid β] :

                                                          Transfer CommMonoid across an Equiv

                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • Equiv.instAddCommMonoidShrink = (equivShrink α).symm.addCommMonoid
                                                            noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [Small.{v, u} α] [CommMonoid α] :
                                                            Equations
                                                            • Equiv.instCommMonoidShrink = (equivShrink α).symm.commMonoid
                                                            theorem Equiv.addGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            e (e.symm 0) = 0
                                                            theorem Equiv.addGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                                            theorem Equiv.addGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                            theorem Equiv.addGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                            theorem Equiv.addGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
                                                            theorem Equiv.addGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            ∀ (x : α), e (e.symm (-e x)) = -e x
                                                            @[reducible, inline]
                                                            abbrev Equiv.addGroup {α : Type u} {β : Type v} (e : α β) [AddGroup β] :

                                                            Transfer AddGroup across an Equiv

                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev Equiv.group {α : Type u} {β : Type v} (e : α β) [Group β] :

                                                              Transfer Group across an Equiv

                                                              Equations
                                                              Instances For
                                                                noncomputable instance Equiv.instAddGroupShrink {α : Type u} [Small.{v, u} α] [AddGroup α] :
                                                                Equations
                                                                noncomputable instance Equiv.instGroupShrink {α : Type u} [Small.{v, u} α] [Group α] :
                                                                Equations
                                                                theorem Equiv.addCommGroup.proof_4 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
                                                                theorem Equiv.addCommGroup.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                                                theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                ∀ (x : α), e (e.symm (-e x)) = -e x
                                                                @[reducible, inline]
                                                                abbrev Equiv.addCommGroup {α : Type u} {β : Type v} (e : α β) [AddCommGroup β] :

                                                                Transfer AddCommGroup across an Equiv

                                                                Equations
                                                                Instances For
                                                                  theorem Equiv.addCommGroup.proof_5 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                  ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                                  theorem Equiv.addCommGroup.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                  e (e.symm 0) = 0
                                                                  theorem Equiv.addCommGroup.proof_6 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                  ∀ (x : α) (n : ), e (e.symm (n e x)) = n e x
                                                                  @[reducible, inline]
                                                                  abbrev Equiv.commGroup {α : Type u} {β : Type v} (e : α β) [CommGroup β] :

                                                                  Transfer CommGroup across an Equiv

                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • Equiv.instAddCommGroupShrink = (equivShrink α).symm.addCommGroup
                                                                    noncomputable instance Equiv.instCommGroupShrink {α : Type u} [Small.{v, u} α] [CommGroup α] :
                                                                    Equations
                                                                    @[reducible, inline]

                                                                    Transfer NonUnitalNonAssocSemiring across an Equiv

                                                                    Equations
                                                                    Instances For
                                                                      Equations
                                                                      • Equiv.instNonUnitalNonAssocSemiringShrink = (equivShrink α).symm.nonUnitalNonAssocSemiring
                                                                      @[reducible, inline]
                                                                      abbrev Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α β) [NonUnitalSemiring β] :

                                                                      Transfer NonUnitalSemiring across an Equiv

                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        • Equiv.instNonUnitalSemiringShrink = (equivShrink α).symm.nonUnitalSemiring
                                                                        @[reducible, inline]
                                                                        abbrev Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α β) [AddMonoidWithOne β] :

                                                                        Transfer AddMonoidWithOne across an Equiv

                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          • Equiv.instAddMonoidWithOneShrink = (equivShrink α).symm.addMonoidWithOne
                                                                          @[reducible, inline]
                                                                          abbrev Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α β) [AddGroupWithOne β] :

                                                                          Transfer AddGroupWithOne across an Equiv

                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            • Equiv.instAddGroupWithOneShrink = (equivShrink α).symm.addGroupWithOne
                                                                            @[reducible, inline]
                                                                            abbrev Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α β) [NonAssocSemiring β] :

                                                                            Transfer NonAssocSemiring across an Equiv

                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              • Equiv.instNonAssocSemiringShrink = (equivShrink α).symm.nonAssocSemiring
                                                                              @[reducible, inline]
                                                                              abbrev Equiv.semiring {α : Type u} {β : Type v} (e : α β) [Semiring β] :

                                                                              Transfer Semiring across an Equiv

                                                                              Equations
                                                                              Instances For
                                                                                noncomputable instance Equiv.instSemiringShrink {α : Type u} [Small.{v, u} α] [Semiring α] :
                                                                                Equations
                                                                                @[reducible, inline]

                                                                                Transfer NonUnitalCommSemiring across an Equiv

                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  • Equiv.instNonUnitalCommSemiringShrink = (equivShrink α).symm.nonUnitalCommSemiring
                                                                                  @[reducible, inline]
                                                                                  abbrev Equiv.commSemiring {α : Type u} {β : Type v} (e : α β) [CommSemiring β] :

                                                                                  Transfer CommSemiring across an Equiv

                                                                                  Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                    • Equiv.instCommSemiringShrink = (equivShrink α).symm.commSemiring
                                                                                    @[reducible, inline]

                                                                                    Transfer NonUnitalNonAssocRing across an Equiv

                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      • Equiv.instNonUnitalNonAssocRingShrink = (equivShrink α).symm.nonUnitalNonAssocRing
                                                                                      @[reducible, inline]
                                                                                      abbrev Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α β) [NonUnitalRing β] :

                                                                                      Transfer NonUnitalRing across an Equiv

                                                                                      Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                        • Equiv.instNonUnitalRingShrink = (equivShrink α).symm.nonUnitalRing
                                                                                        @[reducible, inline]
                                                                                        abbrev Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α β) [NonAssocRing β] :

                                                                                        Transfer NonAssocRing across an Equiv

                                                                                        Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                          • Equiv.instNonAssocRingShrink = (equivShrink α).symm.nonAssocRing
                                                                                          @[reducible, inline]
                                                                                          abbrev Equiv.ring {α : Type u} {β : Type v} (e : α β) [Ring β] :
                                                                                          Ring α

                                                                                          Transfer Ring across an Equiv

                                                                                          Equations
                                                                                          Instances For
                                                                                            noncomputable instance Equiv.instRingShrink {α : Type u} [Small.{v, u} α] [Ring α] :
                                                                                            Equations
                                                                                            @[reducible, inline]
                                                                                            abbrev Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α β) [NonUnitalCommRing β] :

                                                                                            Transfer NonUnitalCommRing across an Equiv

                                                                                            Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                              • Equiv.instNonUnitalCommRingShrink = (equivShrink α).symm.nonUnitalCommRing
                                                                                              @[reducible, inline]
                                                                                              abbrev Equiv.commRing {α : Type u} {β : Type v} (e : α β) [CommRing β] :

                                                                                              Transfer CommRing across an Equiv

                                                                                              Equations
                                                                                              Instances For
                                                                                                noncomputable instance Equiv.instCommRingShrink {α : Type u} [Small.{v, u} α] [CommRing α] :
                                                                                                Equations
                                                                                                theorem Equiv.nontrivial {α : Type u} {β : Type v} (e : α β) [Nontrivial β] :

                                                                                                Transfer Nontrivial across an Equiv

                                                                                                noncomputable instance Equiv.instNontrivialShrink {α : Type u} [Small.{v, u} α] [Nontrivial α] :
                                                                                                Equations
                                                                                                • =
                                                                                                theorem Equiv.isDomain {α : Type u} {β : Type v} [Ring α] [Ring β] [IsDomain β] (e : α ≃+* β) :

                                                                                                Transfer IsDomain across an Equiv

                                                                                                noncomputable instance Equiv.instIsDomainShrink {α : Type u} [Small.{v, u} α] [Ring α] [IsDomain α] :
                                                                                                Equations
                                                                                                • =
                                                                                                @[reducible, inline]
                                                                                                abbrev Equiv.nnratCast {α : Type u} {β : Type v} (e : α β) [NNRatCast β] :

                                                                                                Transfer NNRatCast across an Equiv

                                                                                                Equations
                                                                                                • e.nnratCast = { nnratCast := fun (q : ℚ≥0) => e.symm q }
                                                                                                Instances For
                                                                                                  @[reducible, inline]
                                                                                                  abbrev Equiv.ratCast {α : Type u} {β : Type v} (e : α β) [RatCast β] :

                                                                                                  Transfer RatCast across an Equiv

                                                                                                  Equations
                                                                                                  • e.ratCast = { ratCast := fun (n : ) => e.symm n }
                                                                                                  Instances For
                                                                                                    noncomputable instance Shrink.instNNRatCast {α : Type u} [Small.{v, u} α] [NNRatCast α] :
                                                                                                    Equations
                                                                                                    noncomputable instance Shrink.instRatCast {α : Type u} [Small.{v, u} α] [RatCast α] :
                                                                                                    Equations
                                                                                                    @[reducible, inline]
                                                                                                    abbrev Equiv.divisionRing {α : Type u} {β : Type v} (e : α β) [DivisionRing β] :

                                                                                                    Transfer DivisionRing across an Equiv

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      • Equiv.instDivisionRingShrink = (equivShrink α).symm.divisionRing
                                                                                                      @[reducible, inline]
                                                                                                      abbrev Equiv.field {α : Type u} {β : Type v} (e : α β) [Field β] :

                                                                                                      Transfer Field across an Equiv

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        noncomputable instance Equiv.instFieldShrink {α : Type u} [Small.{v, u} α] [Field α] :
                                                                                                        Equations
                                                                                                        @[reducible, inline]
                                                                                                        abbrev Equiv.mulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α β) [MulAction R β] :

                                                                                                        Transfer MulAction across an Equiv

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          noncomputable instance Equiv.instMulActionShrink {α : Type u} (R : Type u_1) [Monoid R] [Small.{v, u} α] [MulAction R α] :
                                                                                                          Equations
                                                                                                          @[reducible, inline]
                                                                                                          abbrev Equiv.distribMulAction {α : Type u} {β : Type v} (R : Type u_1) [Monoid R] (e : α β) [AddCommMonoid β] [DistribMulAction R β] :

                                                                                                          Transfer DistribMulAction across an Equiv

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[reducible, inline]
                                                                                                            abbrev Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α β) [AddCommMonoid β] :
                                                                                                            let addCommMonoid := e.addCommMonoid; [inst : Module R β] → Module R α

                                                                                                            Transfer Module across an Equiv

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              noncomputable instance Equiv.instModuleShrink {α : Type u} (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] :
                                                                                                              Equations
                                                                                                              def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α β) [AddCommMonoid β] [Module R β] :
                                                                                                              let addCommMonoid := e.addCommMonoid; let module := Equiv.module R e; α ≃ₗ[R] β

                                                                                                              An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β where the R-module structure on α is the one obtained by transporting an R-module structure on β back along e.

                                                                                                              Equations
                                                                                                              • Equiv.linearEquiv R e = { toFun := e.addEquiv.toFun, map_add' := , map_smul' := , invFun := e.addEquiv.invFun, left_inv := , right_inv := }
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem Shrink.linearEquiv_symm_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] :
                                                                                                                ∀ (a : α), (Shrink.linearEquiv α R).symm a = (AddEquiv.symm (equivShrink α).symm.addEquiv) a
                                                                                                                @[simp]
                                                                                                                theorem Shrink.linearEquiv_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] :
                                                                                                                ∀ (a : Shrink.{v, u} α), (Shrink.linearEquiv α R) a = (equivShrink α).symm a
                                                                                                                noncomputable def Shrink.linearEquiv (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] :

                                                                                                                Shrink α to a smaller universe preserves module structure.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[reducible, inline]
                                                                                                                  abbrev Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] :
                                                                                                                  let semiring := e.semiring; [inst : Algebra R β] → Algebra R α

                                                                                                                  Transfer Algebra across an Equiv

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    theorem Equiv.algebraMap_def {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] [Algebra R β] (r : R) :
                                                                                                                    let semiring := e.semiring; let algebra := Equiv.algebra R e; (algebraMap R α) r = e.symm ((algebraMap R β) r)
                                                                                                                    noncomputable instance Equiv.instAlgebraShrink {α : Type u} (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] :
                                                                                                                    Equations
                                                                                                                    def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] [Algebra R β] :
                                                                                                                    let semiring := e.semiring; let algebra := Equiv.algebra R e; α ≃ₐ[R] β

                                                                                                                    An equivalence e : α ≃ β gives an algebra equivalence α ≃ₐ[R] β where the R-algebra structure on α is the one obtained by transporting an R-algebra structure on β back along e.

                                                                                                                    Equations
                                                                                                                    • Equiv.algEquiv R e = { toEquiv := e.ringEquiv.toEquiv, map_mul' := , map_add' := , commutes' := }
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem Equiv.algEquiv_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] [Algebra R β] (a : α) :
                                                                                                                      (Equiv.algEquiv R e) a = e a
                                                                                                                      theorem Equiv.algEquiv_symm_apply {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] [Algebra R β] (b : β) :
                                                                                                                      (AlgEquiv.symm (Equiv.algEquiv R e)) b = e.symm b
                                                                                                                      @[simp]
                                                                                                                      theorem Shrink.algEquiv_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] :
                                                                                                                      ∀ (a : Shrink.{v, u} α), (Shrink.algEquiv α R) a = (equivShrink α).symm a
                                                                                                                      @[simp]
                                                                                                                      theorem Shrink.algEquiv_symm_apply (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] :
                                                                                                                      ∀ (a : α), (Shrink.algEquiv α R).symm a = (equivShrink α) a
                                                                                                                      noncomputable def Shrink.algEquiv (α : Type u) (R : Type u_1) [CommSemiring R] [Small.{v, u} α] [Semiring α] [Algebra R α] :

                                                                                                                      Shrink α to a smaller universe preserves algebra structure.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        theorem Finite.exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
                                                                                                                        ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

                                                                                                                        Any finite group in universe u is equivalent to some finite group in universe v.