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 mark them @[reducible]. See note [reducible non-instances].

Tags #

equiv, group, ring, field, module, algebra

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

Transfer Zero across an Equiv

Equations
Instances For
    @[reducible]
    def Equiv.one {α : Type u} {β : Type v} (e : α β) [One β] :
    One α

    Transfer One across an Equiv

    Equations
    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]
      def Equiv.add {α : Type u} {β : Type v} (e : α β) [Add β] :
      Add α

      Transfer Add across an Equiv

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

        Transfer Mul across an Equiv

        Equations
        • Equiv.mul e = { 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]
          def Equiv.sub {α : Type u} {β : Type v} (e : α β) [Sub β] :
          Sub α

          Transfer Sub across an Equiv

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

            Transfer Div across an Equiv

            Equations
            • Equiv.div e = { 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]
              def Equiv.Neg {α : Type u} {β : Type v} (e : α β) [Neg β] :
              Neg α

              Transfer Neg across an Equiv

              Equations
              Instances For
                @[reducible]
                def Equiv.Inv {α : Type u} {β : Type v} (e : α β) [Inv β] :
                Inv α

                Transfer Inv across an Equiv

                Equations
                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]
                  def Equiv.smul {α : Type u} {β : Type v} (e : α β) (R : Type u_1) [SMul R β] :
                  SMul R α

                  Transfer SMul across an Equiv

                  Equations
                  • Equiv.smul e 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
                    • Equiv.pow e 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 := Equiv.add e; α ≃+ β

                      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
                      Instances For
                        def Equiv.mulEquiv {α : Type u} {β : Type v} (e : α β) [Mul β] :
                        let mul := Equiv.mul e; α ≃* β

                        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
                        Instances For
                          @[simp]
                          theorem Equiv.addEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] (a : α) :
                          (Equiv.addEquiv e) a = e a
                          @[simp]
                          theorem Equiv.mulEquiv_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (a : α) :
                          (Equiv.mulEquiv e) a = e a
                          theorem Equiv.addEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] (b : β) :
                          (AddEquiv.symm (Equiv.addEquiv e)) b = e.symm b
                          theorem Equiv.mulEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Mul β] (b : β) :
                          (MulEquiv.symm (Equiv.mulEquiv e)) 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 := Equiv.add e; let mul := Equiv.mul e; α ≃+* β

                              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
                              Instances For
                                @[simp]
                                theorem Equiv.ringEquiv_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (a : α) :
                                (Equiv.ringEquiv e) a = e a
                                theorem Equiv.ringEquiv_symm_apply {α : Type u} {β : Type v} (e : α β) [Add β] [Mul β] (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]
                                  def Equiv.addSemigroup {α : Type u} {β : Type v} (e : α β) [AddSemigroup β] :

                                  Transfer add_semigroup across an Equiv

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

                                    Transfer Semigroup across an Equiv

                                    Equations
                                    Instances For
                                      Equations
                                      noncomputable instance Equiv.instSemigroupShrink {α : Type u} [Small.{v, u} α] [Semigroup α] :
                                      Equations
                                      @[reducible]
                                      def Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α β) [SemigroupWithZero β] :

                                      Transfer SemigroupWithZero across an Equiv

                                      Equations
                                      Instances For
                                        Equations
                                        Equations
                                        @[reducible]
                                        def 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]
                                          def Equiv.commSemigroup {α : Type u} {β : Type v} (e : α β) [CommSemigroup β] :

                                          Transfer CommSemigroup across an Equiv

                                          Equations
                                          Instances For
                                            Equations
                                            Equations
                                            @[reducible]
                                            def Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α β) [MulZeroClass β] :

                                            Transfer MulZeroClass across an Equiv

                                            Equations
                                            Instances For
                                              Equations
                                              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
                                              theorem Equiv.addZeroClass.proof_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddZeroClass β] :
                                              e (e.symm 0) = 0
                                              @[reducible]
                                              def Equiv.addZeroClass {α : Type u} {β : Type v} (e : α β) [AddZeroClass β] :

                                              Transfer AddZeroClass across an Equiv

                                              Equations
                                              Instances For
                                                @[reducible]
                                                def Equiv.mulOneClass {α : Type u} {β : Type v} (e : α β) [MulOneClass β] :

                                                Transfer MulOneClass across an Equiv

                                                Equations
                                                Instances For
                                                  Equations
                                                  noncomputable instance Equiv.instMulOneClassShrink {α : Type u} [Small.{v, u} α] [MulOneClass α] :
                                                  Equations
                                                  @[reducible]
                                                  def Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α β) [MulZeroOneClass β] :

                                                  Transfer MulZeroOneClass across an Equiv

                                                  Equations
                                                  Instances For
                                                    Equations
                                                    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_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddMonoid β] :
                                                    e (e.symm 0) = 0
                                                    @[reducible]
                                                    def Equiv.addMonoid {α : Type u} {β : Type v} (e : α β) [AddMonoid β] :

                                                    Transfer AddMonoid across an Equiv

                                                    Equations
                                                    Instances For
                                                      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]
                                                      def 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_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommMonoid β] :
                                                        e (e.symm 0) = 0
                                                        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_2 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommMonoid β] :
                                                        ∀ (x y : α), e (e.symm (e x + e y)) = e x + e y
                                                        @[reducible]
                                                        def Equiv.addCommMonoid {α : Type u} {β : Type v} (e : α β) [AddCommMonoid β] :

                                                        Transfer AddCommMonoid across an Equiv

                                                        Equations
                                                        Instances For
                                                          @[reducible]
                                                          def Equiv.commMonoid {α : Type u} {β : Type v} (e : α β) [CommMonoid β] :

                                                          Transfer CommMonoid across an Equiv

                                                          Equations
                                                          Instances For
                                                            Equations
                                                            noncomputable instance Equiv.instCommMonoidShrink {α : Type u} [Small.{v, u} α] [CommMonoid α] :
                                                            Equations
                                                            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_1 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                            e (e.symm 0) = 0
                                                            @[reducible]
                                                            def Equiv.addGroup {α : Type u} {β : Type v} (e : α β) [AddGroup β] :

                                                            Transfer AddGroup across an Equiv

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              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_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                              ∀ (x : α), e (e.symm (-e x)) = -e x
                                                              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_4 {α : Type u_2} {β : Type u_1} (e : α β) [AddGroup β] :
                                                              ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
                                                              @[reducible]
                                                              def Equiv.group {α : Type u} {β : Type v} (e : α β) [Group β] :

                                                              Transfer Group across an Equiv

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              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_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_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
                                                                theorem Equiv.addCommGroup.proof_3 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                ∀ (x : α), e (e.symm (-e x)) = -e x
                                                                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_4 {α : Type u_2} {β : Type u_1} (e : α β) [AddCommGroup β] :
                                                                ∀ (x y : α), e (e.symm (e x - e y)) = e x - e y
                                                                @[reducible]
                                                                def Equiv.addCommGroup {α : Type u} {β : Type v} (e : α β) [AddCommGroup β] :

                                                                Transfer AddCommGroup across an Equiv

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[reducible]
                                                                  def Equiv.commGroup {α : Type u} {β : Type v} (e : α β) [CommGroup β] :

                                                                  Transfer CommGroup across an Equiv

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    noncomputable instance Equiv.instCommGroupShrink {α : Type u} [Small.{v, u} α] [CommGroup α] :
                                                                    Equations
                                                                    @[reducible]

                                                                    Transfer NonUnitalNonAssocSemiring across an Equiv

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Equations
                                                                      @[reducible]
                                                                      def Equiv.nonUnitalSemiring {α : Type u} {β : Type v} (e : α β) [NonUnitalSemiring β] :

                                                                      Transfer NonUnitalSemiring across an Equiv

                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        @[reducible]
                                                                        def Equiv.addMonoidWithOne {α : Type u} {β : Type v} (e : α β) [AddMonoidWithOne β] :

                                                                        Transfer AddMonoidWithOne across an Equiv

                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          @[reducible]
                                                                          def Equiv.addGroupWithOne {α : Type u} {β : Type v} (e : α β) [AddGroupWithOne β] :

                                                                          Transfer AddGroupWithOne across an Equiv

                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            @[reducible]
                                                                            def Equiv.nonAssocSemiring {α : Type u} {β : Type v} (e : α β) [NonAssocSemiring β] :

                                                                            Transfer NonAssocSemiring across an Equiv

                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              @[reducible]
                                                                              def 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]

                                                                                Transfer NonUnitalCommSemiring across an Equiv

                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  @[reducible]
                                                                                  def Equiv.commSemiring {α : Type u} {β : Type v} (e : α β) [CommSemiring β] :

                                                                                  Transfer CommSemiring across an Equiv

                                                                                  Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                    @[reducible]

                                                                                    Transfer NonUnitalNonAssocRing across an Equiv

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      Equations
                                                                                      @[reducible]
                                                                                      def Equiv.nonUnitalRing {α : Type u} {β : Type v} (e : α β) [NonUnitalRing β] :

                                                                                      Transfer NonUnitalRing across an Equiv

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        @[reducible]
                                                                                        def Equiv.nonAssocRing {α : Type u} {β : Type v} (e : α β) [NonAssocRing β] :

                                                                                        Transfer NonAssocRing across an Equiv

                                                                                        Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                          @[reducible]
                                                                                          def 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]
                                                                                            def Equiv.nonUnitalCommRing {α : Type u} {β : Type v} (e : α β) [NonUnitalCommRing β] :

                                                                                            Transfer NonUnitalCommRing across an Equiv

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              Equations
                                                                                              @[reducible]
                                                                                              def 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
                                                                                                @[reducible]
                                                                                                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
                                                                                                • =
                                                                                                @[reducible]
                                                                                                theorem Equiv.isDomain {α : Type u} {β : Type v} [Ring α] [Ring β] [IsDomain β] (e : α ≃+* β) :

                                                                                                Transfer IsDomain across an Equiv

                                                                                                Equations
                                                                                                • =
                                                                                                @[reducible]
                                                                                                def Equiv.RatCast {α : Type u} {β : Type v} (e : α β) [RatCast β] :

                                                                                                Transfer RatCast across an Equiv

                                                                                                Equations
                                                                                                Instances For
                                                                                                  noncomputable instance Equiv.instRatCastShrink {α : Type u} [Small.{v, u} α] [RatCast α] :
                                                                                                  Equations
                                                                                                  @[reducible]
                                                                                                  def Equiv.divisionRing {α : Type u} {β : Type v} (e : α β) [DivisionRing β] :

                                                                                                  Transfer DivisionRing across an Equiv

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    @[reducible]
                                                                                                    def Equiv.field {α : Type u} {β : Type v} (e : α β) [Field β] :

                                                                                                    Transfer Field across an Equiv

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      noncomputable instance Equiv.instFieldShrink {α : Type u} [Small.{v, u} α] [Field α] :
                                                                                                      Equations
                                                                                                      @[reducible]
                                                                                                      def 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]
                                                                                                        def 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]
                                                                                                          def Equiv.module {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α β) [AddCommMonoid β] :
                                                                                                          let addCommMonoid := Equiv.addCommMonoid e; [inst : Module R β] → Module R α

                                                                                                          Transfer Module across an Equiv

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def Equiv.linearEquiv {α : Type u} {β : Type v} (R : Type u_1) [Semiring R] (e : α β) [AddCommMonoid β] [Module R β] :
                                                                                                            let addCommMonoid := Equiv.addCommMonoid e; 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
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem Shrink.linearEquiv_symm_apply (α : Type u) (R : Type u_1) [Semiring R] [Small.{v, u} α] [AddCommMonoid α] [Module R α] :
                                                                                                              @[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]
                                                                                                                def Equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] :
                                                                                                                let semiring := Equiv.semiring e; [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 := Equiv.semiring e; let algebra := Equiv.algebra R e; (algebraMap R α) r = e.symm ((algebraMap R β) r)
                                                                                                                  def Equiv.algEquiv {α : Type u} {β : Type v} (R : Type u_1) [CommSemiring R] (e : α β) [Semiring β] [Algebra R β] :
                                                                                                                  let semiring := Equiv.semiring e; 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
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  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 : α), (AlgEquiv.symm (Shrink.algEquiv α R)) 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_zero_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
                                                                                                                      ∃ (G' : Type) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

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