Loogle!

Result

Found 56 declarations mentioning MulEquiv and Equiv.symm. Of these, 44 have a name containing "symm".

• MulEquiv.symm.eq_1 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) : h.symm = { toEquiv := h.symm, map_mul' := ⋯ }
• MulEquiv.toEquiv_symm 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : ↑f.symm = (↑f).symm
• MulEquiv.coe_toEquiv_symm 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : ⇑(↑f).symm = ⇑f.symm
• MulEquiv.symm_mk 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) : { toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := ⋯ }
• MulEquiv.symm_map_mul 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) (x y : N) : h.symm (x * y) = h.symm x * h.symm y
• MulEquiv.symmEquiv_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.Defs
  (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : P) : ((MulEquiv.symmEquiv P Q).symm h) a✝ = h.symm a✝
• MulEquiv.symmEquiv_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Defs
  (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : Q) : ((MulEquiv.symmEquiv P Q).symm h).symm a✝ = h a✝
• AddEquiv.toMultiplicativeLeft_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : Multiplicative G ≃* H) (a : G) : (AddEquiv.toMultiplicativeLeft.symm f) a = (MonoidHom.toAdditiveRight f.toMonoidHom) a
• AddEquiv.toMultiplicativeRight_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : G ≃* Multiplicative H) (a : Additive G) : (AddEquiv.toMultiplicativeRight.symm f) a = (MonoidHom.toAdditiveLeft f.toMonoidHom) a
• AddEquiv.toMultiplicative_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : Multiplicative G ≃* Multiplicative H) (a : G) : (AddEquiv.toMultiplicative.symm f) a = (AddMonoidHom.toMultiplicative.symm f.toMonoidHom) a
• MulEquiv.toAdditive_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : Additive G ≃+ Additive H) (a : G) : (MulEquiv.toAdditive.symm f) a = (MonoidHom.toAdditive.symm f.toAddMonoidHom) a
• AddEquiv.toMultiplicativeRight_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : G ≃* Multiplicative H) (a : H) : (AddEquiv.toMultiplicativeRight.symm f).symm a = (MonoidHom.toAdditiveRight f.symm.toMonoidHom) a
• AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : Multiplicative G ≃* H) (a : Additive H) : (AddEquiv.toMultiplicativeLeft.symm f).symm a = (MonoidHom.toAdditiveLeft f.symm.toMonoidHom) a
• AddEquiv.toMultiplicative_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : Multiplicative G ≃* Multiplicative H) (a : H) : (AddEquiv.toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) a
• MulEquiv.toAdditive_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.TypeTags
  {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : Additive G ≃+ Additive H) (a : H) : (MulEquiv.toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a
• MulEquiv.coe_prodAssoc_symm 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] : ⇑MulEquiv.prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm
• MulEquiv.symm_monoidHomCongrLeftEquiv 📋 Mathlib.Algebra.Group.Equiv.Basic
  {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) : e.monoidHomCongrLeftEquiv.symm = e.symm.monoidHomCongrLeftEquiv
• MulEquiv.symm_monoidHomCongrRightEquiv 📋 Mathlib.Algebra.Group.Equiv.Basic
  {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) : e.monoidHomCongrRightEquiv.symm = e.symm.monoidHomCongrRightEquiv
• MulEquiv.monoidHomCongrLeftEquiv_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Basic
  {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) (f : M₂ →* N) : e.monoidHomCongrLeftEquiv.symm f = f.comp e.toMonoidHom
• MulEquiv.monoidHomCongrRightEquiv_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Basic
  {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₂) : e.monoidHomCongrRightEquiv.symm hmn = e.symm.toMonoidHom.comp hmn
• MonoidHom.postcompEquiv_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Basic
  {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (g : γ →* β) : (MonoidHom.postcompEquiv e γ).symm g = e.symm.toMonoidHom.comp g
• MonoidHom.precompEquiv_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Basic
  {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (g : α →* γ) : (MonoidHom.precompEquiv e γ).symm g = g.comp ↑e.symm
• Equiv.permCongrHom_symm 📋 Mathlib.Algebra.Group.End
  {α : Type u_4} {β : Type u_5} (e : α ≃ β) : e.permCongrHom.symm = e.symm.permCongrHom
• Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.End
  {α : Type u_4} (u : (Function.End α)ˣ) : ⇑(Equiv.symm (Equiv.Perm.equivUnitsEnd.symm u)) = ↑u⁻¹
• MulEquiv.op_symm_apply_apply 📋 Mathlib.Algebra.Group.Equiv.Opposite
  {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a✝ : α) : (MulEquiv.op.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝
• MulEquiv.op_symm_apply_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Opposite
  {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a✝ : β) : (MulEquiv.op.symm f).symm a✝ = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a✝
• MulEquiv.withZero_symm_apply_apply 📋 Mathlib.Algebra.GroupWithZero.WithZero
  {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : α) : (MulEquiv.withZero.symm e) x = WithZero.unzero ⋯
• MulEquiv.withZero_symm_apply_symm_apply 📋 Mathlib.Algebra.GroupWithZero.WithZero
  {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : β) : (MulEquiv.withZero.symm e).symm x = WithZero.unzero ⋯
• MulEquiv.submonoidMap_symm_apply 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : ↥(Submonoid.map (↑e) S)) : (e.submonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩
• MulEquiv.subgroupMap_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥(Subgroup.map (↑e) H)) : (e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
• FreeMonoid.freeMonoidCongr_symm_of 📋 Mathlib.Algebra.FreeMonoid.Basic
  {α : Type u_6} {β : Type u_7} (e : α ≃ β) (b : β) : (FreeMonoid.freeMonoidCongr e.symm) (FreeMonoid.of b) = FreeMonoid.of (e.symm b)
• FreeGroup.freeGroupCongr_symm 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) : (FreeGroup.freeGroupCongr e).symm = FreeGroup.freeGroupCongr e.symm
• OrderMonoidIso.withZero_symm_apply_symm_apply 📋 Mathlib.Algebra.Order.Hom.MonoidWithZero
  {G : Type u_6} {H : Type u_7} [Group G] [PartialOrder G] [Group H] [PartialOrder H] (e : WithZero G ≃*o WithZero H) (x : H) : (OrderMonoidIso.withZero.symm e).symm x = WithZero.unzero ⋯
• Equiv.mulEquiv_symm_apply 📋 Mathlib.Algebra.Group.TransferInstance
  {α : Type u_2} {β : Type u_3} (e : α ≃ β) [Mul β] (b : β) : (MulEquiv.symm e.mulEquiv) b = e.symm b
• Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)
• Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑(↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x))⁻¹ = 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)
• uliftZPowersHom_symm_apply 📋 Mathlib.Algebra.Category.Grp.ForgetCorepresentable
  (G : Type u) [Group G] (a✝ : ULift.{u, 0} (Multiplicative ℤ) →* G) : (uliftZPowersHom G).symm a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
• uliftPowersHom_symm_apply 📋 Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
  (M : Type u) [Monoid M] (a✝ : ULift.{u, 0} (Multiplicative ℕ) →* M) : (uliftPowersHom M).symm a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
• UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply 📋 Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
  {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a : α} {q : β} (hq : q ∈ UniqueFactorizationMonoid.normalizedFactors (f a)) : ↑((UniqueFactorizationMonoid.normalizedFactorsEquiv he a).symm ⟨q, hq⟩) = (↑f).symm q
• mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe 📋 Mathlib.RingTheory.ChainOfDivisors
  {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] {m : M} {n : N} {d : { l // l ∣ m } ≃ { l // l ∣ n }} (hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') (l : ↑(Set.Iic (Associates.mk n))) : ↑((RelIso.symm (mkFactorOrderIsoOfFactorDvdEquiv hd)) l) = Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)
• Subgroup.IsComplement'.QuotientMulEquiv_symm_apply 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) (a✝ : ↥H) : h.QuotientMulEquiv.symm a✝ = (Subgroup.IsComplement.leftQuotientEquiv h).symm a✝
• FreeGroupBasis.lift_symm_apply 📋 Mathlib.GroupTheory.FreeGroup.IsFreeGroup
  {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (a✝ : G →* H) (a✝¹ : ι) : b.lift.symm a✝ a✝¹ = a✝ (b.repr.symm (FreeGroup.of a✝¹))
• PresentedGroup.equivPresentedGroup_symm_apply_of 📋 Mathlib.GroupTheory.PresentedGroup
  {α : Type u_1} {β : Type u_3} (x : β) (rels : Set (FreeGroup α)) (e : α ≃ β) : (PresentedGroup.equivPresentedGroup rels e).symm (PresentedGroup.of x) = PresentedGroup.of (e.symm x)
• HNNExtension.NormalWord.unitsSMulEquiv_symm_apply 📋 Mathlib.GroupTheory.HNNExtension
  {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (w : HNNExtension.NormalWord d) : (HNNExtension.NormalWord.unitsSMulEquiv φ).symm w = HNNExtension.NormalWord.unitsSMul φ (-1) w

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 519f454