Loogle!

Result

Found 42 declarations mentioning Units.map.

• Units.map 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) : Mˣ →* Nˣ
• Units.map_id 📋 Mathlib.Algebra.Group.Units.Hom
  (M : Type u) [Monoid M] : Units.map (MonoidHom.id M) = MonoidHom.id Mˣ
• Units.map_injective 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(Units.map f)
• Units.map_comp 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} {P : Type w} [Monoid M] [Monoid N] [Monoid P] (f : M →* N) (g : N →* P) : Units.map (g.comp f) = (Units.map g).comp (Units.map f)
• Units.coe_map 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (x : Mˣ) : ↑((Units.map f) x) = f ↑x
• Units.coe_map_inv 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (u : Mˣ) : ↑((Units.map f) u)⁻¹ = f ↑u⁻¹
• Units.map.eq_1 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) : Units.map f = MonoidHom.mk' (fun u => { val := f ↑u, inv := f u.inv, val_inv := ⋯, inv_val := ⋯ }) ⋯
• Units.map_mk 📋 Mathlib.Algebra.Group.Units.Hom
  {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (val inv : M) (val_inv : val * inv = 1) (inv_val : inv * val = 1) : (Units.map f) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } = { val := f val, inv := f inv, val_inv := ⋯, inv_val := ⋯ }
• MulEquiv.prodUnits.eq_1 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] : MulEquiv.prodUnits = { toFun := ⇑((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))), invFun := fun u => { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ }, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
• Units.map_neg_one 📋 Mathlib.Algebra.Ring.Units
  {α : Type u} {β : Type v} [Ring α] {F : Type u_1} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) : (Units.map ↑f) (-1) = -1
• Units.map_neg 📋 Mathlib.Algebra.Ring.Units
  {α : Type u} {β : Type v} [Ring α] {F : Type u_1} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) (u : αˣ) : (Units.map ↑f) (-u) = -(Units.map ↑f) u
• unitsCenterToCenterUnits.eq_1 📋 Mathlib.GroupTheory.Submonoid.Center
  (M : Type u_1) [Monoid M] : unitsCenterToCenterUnits M = (Units.map (Submonoid.center M).subtype).codRestrict (Submonoid.center Mˣ) ⋯
• Algebra.smul_units_def 📋 Mathlib.Algebra.Algebra.Hom
  {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (f : A →ₐ[R] A) (x : Aˣ) : f • x = (Units.map ↑f) x
• AlgEquiv.smul_units_def 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) : f • x = (Units.map ↑f) x
• unitsNonZeroDivisorsEquiv_apply 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  {M₀ : Type u_1} [MonoidWithZero M₀] (a✝ : (↥(nonZeroDivisors M₀))ˣ) : unitsNonZeroDivisorsEquiv a✝ = (↑(Units.map (nonZeroDivisors M₀).subtype)).toFun a✝
• Continuous.units_map 📋 Mathlib.Topology.Algebra.Monoid
  {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →* N) (hf : Continuous ⇑f) : Continuous ⇑(Units.map f)
• IsLocalRing.surjective_units_map_of_local_ringHom 📋 Mathlib.RingTheory.LocalRing.RingHom.Basic
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) (h : IsLocalHom f) : Function.Surjective ⇑(Units.map ↑f)
• LocalRing.surjective_units_map_of_local_ringHom 📋 Mathlib.RingTheory.LocalRing.RingHom.Basic
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) (h : IsLocalHom f) : Function.Surjective ⇑(Units.map ↑f)
• Matrix.GeneralLinearGroup.map.eq_1 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
  {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : Matrix.GeneralLinearGroup.map f = Units.map ↑f.mapMatrix
• Matrix.GeneralLinearGroup.map_det 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
  {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) : Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map f) g) = (Units.map ↑f) (Matrix.GeneralLinearGroup.det g)
• unitary.toUnits_comp_map 📋 Mathlib.Algebra.Star.Unitary
  {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) : unitary.toUnits.comp (unitary.map f) = (Units.map ↑f).comp unitary.toUnits
• AffineEquiv.linear_equivUnitsAffineMap_symm_apply 📋 Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
  {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) : (AffineEquiv.equivUnitsAffineMap.symm u).linear = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)
• WeierstrassCurve.map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
  {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ' = (Units.map ↑f) W.Δ'
• WeierstrassCurve.inv_map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
  {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ'⁻¹ = (Units.map ↑f) W.Δ'⁻¹
• WeierstrassCurve.VariableChange.map_u 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
  {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : (WeierstrassCurve.VariableChange.map φ C).u = (Units.map ↑φ) C.u
• WeierstrassCurve.VariableChange.map.eq_1 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
  {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.map φ C = { u := (Units.map ↑φ) C.u, r := φ C.r, s := φ C.s, t := φ C.t }
• ClassGroup.mk_canonicalEquiv 📋 Mathlib.RingTheory.ClassGroup
  {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : ClassGroup.mk ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = ClassGroup.mk I
• FractionalIdeal.map_canonicalEquiv_mk0 📋 Mathlib.RingTheory.ClassGroup
  {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))) : (Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) ((FractionalIdeal.mk0 K) I) = (FractionalIdeal.mk0 K') I
• ClassGroup.mk_def 📋 Mathlib.RingTheory.ClassGroup
  {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : ClassGroup.mk I = (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range) ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K (FractionRing R))) I)
• Valuation.unit_map_eq 📋 Mathlib.RingTheory.Valuation.Basic
  {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) (u : Rˣ) : ↑((Units.map ↑v) u) = v ↑u
• ValuationSubring.principalUnitGroupEquiv 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) : ↥A.principalUnitGroup ≃* ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
• ValuationSubring.unitGroupToResidueFieldUnits.eq_1 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) : A.unitGroupToResidueFieldUnits = (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom
• ValuationSubring.coe_mem_principalUnitGroup_iff 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) {x : ↥A.unitGroup} : ↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker
• ValuationSubring.principalUnitGroupEquiv_apply 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A.principalUnitGroup) : ↑↑↑(A.principalUnitGroupEquiv a) = ↑↑a
• ValuationSubring.principalUnitGroup_symm_apply 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker) : ↑↑(A.principalUnitGroupEquiv.symm a) = ↑↑↑a
• IsPrimitiveRoot.map_rootsOfUnity 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {ζ : R} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) {f : F} (hf : Function.Injective ⇑f) : Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S
• FiniteField.unitsMap_norm_surjective 📋 Mathlib.FieldTheory.Finite.GaloisField
  (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] [Finite K'] : Function.Surjective ⇑(Units.map (Algebra.norm K))
• ZMod.unitsMap.eq_1 📋 Mathlib.Data.ZMod.Units
  {n m : ℕ} (hm : n ∣ m) : ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
• ZMod.unitsMap_def 📋 Mathlib.Data.ZMod.Units
  {n m : ℕ} (hm : n ∣ m) : ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
• PowerSeries.map_invUnitsSub 📋 Mathlib.RingTheory.PowerSeries.WellKnown
  {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (u : Rˣ) : (PowerSeries.map f) (PowerSeries.invUnitsSub u) = PowerSeries.invUnitsSub ((Units.map ↑f) u)
• IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq 📋 Mathlib.RingTheory.DedekindDomain.SelmerGroup
  {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Rˣ) : v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1
• IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq 📋 Mathlib.RingTheory.DedekindDomain.SelmerGroup
  {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) (x : Rˣ) : (v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1

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 19971e9 serving mathlib revision bce1d65