chore: export algebraMap from Algebra instead of having a def (leanprover-community#38430)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Algebra/Algebra/Defs.lean

@@ -88,24 +88,17 @@ assert_not_exists Field Finset Module.End
 
 universe u v w u₁ v₁
 
-section Prio
-
 /-- An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.
 
 See the implementation notes in this file for discussion of the details of this definition.
 -/
 class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul R A where
-  /-- Embedding `R →+* A` given by `Algebra` structure.
-  Use `algebraMap` from the root namespace instead. -/
-  protected algebraMap : R →+* A
+  /-- Embedding `R →+* A` given by `Algebra` structure. -/
+  algebraMap (R) (A) : R →+* A
   commutes' : ∀ r x, algebraMap r * x = x * algebraMap r
   smul_def' : ∀ r x, r • x = algebraMap r * x
 
-end Prio
-
-/-- Embedding `R →+* A` given by `Algebra` structure. -/
-def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A :=
-  Algebra.algebraMap
+export Algebra (algebraMap)
 
 theorem Algebra.subsingleton (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A]
     [Subsingleton R] : Subsingleton A :=

Mathlib/Algebra/Algebra/Pi.lean

@@ -250,8 +250,8 @@ end
 end AlgEquiv
 
 /-- Apply an algebra map component-wise along a vector. -/
-def Pi.algebraMap (ι R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
+protected def Pi.algebraMap (ι R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
     (ι → R) →ₗ[R] (ι → A) where
-  toFun v := _root_.algebraMap R A ∘ v
+  toFun v := algebraMap R A ∘ v
   map_add' v w := by simp
   map_smul' t v := by ext; simp [Algebra.smul_def]

Mathlib/Algebra/Star/Subalgebra.lean

@@ -513,7 +513,7 @@ theorem _root_.Subalgebra.starClosure_eq_adjoin (S : Subalgebra R A) :
 @[elab_as_elim]
 theorem adjoin_induction {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop}
     (mem : ∀ (x) (h : x ∈ s), p x (subset_adjoin R s h))
-    (algebraMap : ∀ r, p (_root_.algebraMap R _ r) (_root_.algebraMap_mem _ r))
+    (algebraMap : ∀ r, p (algebraMap R _ r) (algebraMap_mem _ r))
     (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
     (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
     (star : ∀ x hx, p x hx → p (star x) (star_mem hx))
@@ -529,11 +529,11 @@ theorem adjoin_induction₂ {s : Set A} {p : (x y : A) → x ∈ adjoin R s →
     (mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_adjoin R s hx)
       (subset_adjoin R s hy))
     (algebraMap_both : ∀ r₁ r₂, p (algebraMap R A r₁) (algebraMap R A r₂)
-      (_root_.algebraMap_mem _ r₁) (_root_.algebraMap_mem _ r₂))
-    (algebraMap_left : ∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (_root_.algebraMap_mem _ r)
+      (algebraMap_mem _ r₁) (algebraMap_mem _ r₂))
+    (algebraMap_left : ∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (algebraMap_mem _ r)
       (subset_adjoin R s hx))
     (algebraMap_right : ∀ (r) (x) (hx : x ∈ s), p x (algebraMap R A r) (subset_adjoin R s hx)
-      (_root_.algebraMap_mem _ r))
+      (algebraMap_mem _ r))
     (add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
     (add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
     (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)

Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean

@@ -262,7 +262,7 @@ variable {F : Type*} [NormedRing F] [NormedAlgebra ℝ F]
 
 /- A (private) abbreviation introduced for conciseness below.
 We will show that for every `x : F`, `φ x` takes the value zero. -/
-private abbrev φ (x : F) (u : ℝ × ℝ) : F := x ^ 2 - u.1 • x + algebraMap ℝ F u.2
+private noncomputable abbrev φ (x : F) (u : ℝ × ℝ) : F := x ^ 2 - u.1 • x + algebraMap ℝ F u.2
 
 private lemma continuous_φ (x : F) : Continuous (φ x) := by fun_prop
 

Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

@@ -484,7 +484,7 @@ theorem adjoin_induction {s : Set E} {p : ∀ x ∈ adjoin F s, Prop}
     {x} (h : x ∈ adjoin F s) : p x h :=
   Subfield.closure_induction
     (fun x hx ↦ Or.casesOn hx (fun ⟨x, hx⟩ ↦ hx ▸ algebraMap x) (mem x))
-    (by simp_rw [← (_root_.algebraMap F E).map_one]; exact algebraMap 1) add
+    (by simp_rw [← (Algebra.algebraMap F E).map_one]; exact algebraMap 1) add
     (fun x _ h ↦ by
       simp_rw [← neg_one_smul F x, Algebra.smul_def]; exact mul _ _ _ _ (algebraMap _) h) inv mul h
 

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -191,7 +191,7 @@ theorem induction {C : CliffordAlgebra Q → Prop}
       mul_mem' := @mul
       add_mem' := @add
       algebraMap_mem' := algebraMap }
-  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = _root_.algebraMap _ _ (Q m) } :=
+  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = Algebra.algebraMap _ _ (Q m) } :=
     ⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι,
       fun m => Subtype.ext <| ι_sq_scalar Q m⟩
   -- the mapping through the subalgebra is the identity

Mathlib/RingTheory/Localization/Integral.lean

@@ -257,7 +257,7 @@ theorem IsLocalization.scaleRoots_commonDenom_mem_lifts (p : Rₘ[X])
 theorem IsIntegral.exists_multiple_integral_of_isLocalization [Algebra Rₘ S] [IsScalarTower R Rₘ S]
     (x : S) (hx : IsIntegral Rₘ x) : ∃ m : M, IsIntegral R (m • x) := by
   rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
-  · haveI := (_root_.algebraMap Rₘ S).codomain_trivial
+  · haveI := (algebraMap Rₘ S).codomain_trivial
     exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
   obtain ⟨p, hp₁, hp₂⟩ := hx
   -- Porting note: obtain doesn't support side goals

Mathlib/RingTheory/OrderOfVanishing/Basic.lean

@@ -182,7 +182,7 @@ lemma ord_le_ord_mul (a : R) (x : R) : ord R x ≤ ord R (a * x) := by
     let g : (R ⧸ Ideal.span {a * x}) →ₗ[R] (R ⧸ Ideal.span {x}) := Submodule.factor this
     refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)
   rw [Ideal.span_singleton_le_span_singleton]
-  exact Dvd.intro_left (Algebra.algebraMap a) rfl
+  exact Dvd.intro_left (algebraMap R R a) rfl
 
 lemma ord_le_ord_of_dvd {a x : R} (h : a ∣ x) : ord R a ≤ ord R x := by
   obtain ⟨b, rfl⟩ := h

Mathlib/Tactic/Module.lean

@@ -202,7 +202,7 @@ variable (R)
 commutative semiring, by applying to each `S`-component the algebra-map from `S` into a specified
 `S`-algebra `R`. -/
 def algebraMap [CommSemiring S] [Semiring R] [Algebra S R] (l : NF S M) : NF R M :=
-  l.map (fun ⟨s, x⟩ ↦ (_root_.algebraMap S R s, x))
+  l.map (fun ⟨s, x⟩ ↦ (Algebra.algebraMap S R s, x))
 
 theorem eval_algebraMap [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid M] [SMul S M]
     [MulAction R M] [IsScalarTower S R M] (l : NF S M) :

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -237,7 +237,7 @@ lemma le_centralizer_centralizer [T2Space A] (x : A) :
 theorem induction_on {x y : A}
     (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop}
     (self : P x (self_mem R x)) (star_self : P (star x) (star_self_mem R x))
-    (algebraMap : ∀ r, P (algebraMap R A r) (_root_.algebraMap_mem _ r))
+    (algebraMap : ∀ r, P (algebraMap R A r) (algebraMap_mem _ r))
     (add : ∀ u hu v hv, P u hu → P v hv → P (u + v) (add_mem hu hv))
     (mul : ∀ u hu v hv, P u hu → P v hv → P (u * v) (mul_mem hu hv))
     (closure : ∀ s : Set A, (hs : s ⊆ elemental R x) → (∀ u, (hu : u ∈ s) →