chore(data/mv_polynomial/{basic, monad}): move lemmas aeval_X_left …

…and `aeval_X_left_apply` (#16391)
leanprover-community · Sep 14, 2022 · 9532aeb · 9532aeb
1 parent 71b8c46
commit 9532aeb
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
@@ -1110,6 +1110,12 @@ theorem aeval_unique (φ : mv_polynomial σ R →ₐ[R] S₁) :
   φ = aeval (φ ∘ X) :=
 by { ext i, simp }
 
+lemma aeval_X_left : aeval X = alg_hom.id R (mv_polynomial σ R) :=
+(aeval_unique (alg_hom.id R _)).symm
+
+lemma aeval_X_left_apply (p : mv_polynomial σ R) : aeval X p = p :=
+alg_hom.congr_fun aeval_X_left p
+
 lemma comp_aeval {B : Type*} [comm_semiring B] [algebra R B]
   (φ : S₁ →ₐ[R] B) :
   φ.comp (aeval f) = aeval (λ i, φ (f i)) :=

diff --git a/src/data/mv_polynomial/monad.lean b/src/data/mv_polynomial/monad.lean
@@ -133,12 +133,6 @@ eval₂_hom_X' f X i
 lemma bind₁_X_left : bind₁ (X : σ → mv_polynomial σ R) = alg_hom.id R _ :=
 by { ext1 i, simp }
 
-lemma aeval_X_left : aeval (X : σ → mv_polynomial σ R) = alg_hom.id R _ :=
-by rw [aeval_eq_bind₁, bind₁_X_left]
-
-lemma aeval_X_left_apply (φ : mv_polynomial σ R) : aeval X φ = φ :=
-by rw [aeval_eq_bind₁, bind₁_X_left, alg_hom.id_apply]
-
 variable (f : σ → mv_polynomial τ R)
 
 @[simp]