Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M = ⊥
Tactic:
rw [eq_bot_iff]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M ≤ ⊥

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M ≤ ⊥
Tactic:
intro p hp
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ ⊥

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ ⊥
Tactic:
rw [Algebra.mem_bot]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Tactic:
convert Set.mem_range_self ((algebraMapInv R M) p)
State after:
case h.e'_4
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p = (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p)

State before:
case h.e'_4
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p = (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p)
Tactic:
exact (algebraMap_right_inv_of_degree_zero R M ⟨p, hp⟩).symm
State after:
no goals