Some convenient results on neighborhood basis of ℤₚ around 0

Open ideal of ℤₚ

theorem IsDedekindDomain.isOpen_span_singleton_of_ne_zero {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {x : R} (hx : x ≠ 0) : IsOpen ↑(Ideal.span {x})

theorem IsDedekindDomain.isOpen_span_singleton_pow_of_irreducible {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {p : R} (hp : Irreducible p) (n : ℕ) : IsOpen ↑(Ideal.span {p ^ n})

noncomputable def IsDedekindDomain.continuousLinearEquivOfNeZero {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {x : R} (hx : x ≠ 0) : R ≃L[R] ↥(Ideal.span {x})

If x ≠ 0, then R ≃ ⟨x⟩, a ↦ x * a is an isomorphism of topological module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsDedekindDomain.coe_continuousLinearEquivOfNeZero_apply {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {x : R} (hx : x ≠ 0) (a : R) : ↑((continuousLinearEquivOfNeZero hx) a) = x * a

theorem IsDedekindDomain.nonempty_continuousLinearEquiv_of_ne_bot {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] [IsPrincipalIdealRing R] {I : Ideal R} (hI : I ≠ ⊥) : Nonempty (↥I ≃L[R] R)

theorem PadicInt.isOpen_span_p_pow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOpen ↑(Ideal.span {↑p ^ n})

theorem PadicInt.isOpen_pi_span_p_pow (ι : Type u_1) [Finite ι] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsOpen ↑(Ideal.pi fun (x : ι) => Ideal.span {↑p ^ n})

Index of ideals of ℤₚ

theorem PadicInt.index_span_p_pow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (Submodule.toAddSubgroup (Ideal.span {↑p ^ n})).index = p ^ n

theorem PadicInt.index_pi_span_p_pow (ι : Type u_1) [Finite ι] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (Submodule.toAddSubgroup (Ideal.pi fun (x : ι) => Ideal.span {↑p ^ n})).index = p ^ (n * Nat.card ι)

Neighborhood basis of ℤₚ around 0

theorem PadicInt.nhds_zero_hasAntitoneBasis_span_p_pow (p : ℕ) [Fact (Nat.Prime p)] : (nhds 0).HasAntitoneBasis fun (n : ℕ) => ↑(Ideal.span {↑p ^ n})

theorem PadicInt.nhds_zero_hasAntitoneBasis_pi_span_p_pow (ι : Type u_1) [Finite ι] (p : ℕ) [Fact (Nat.Prime p)] : (nhds 0).HasAntitoneBasis fun (n : ℕ) => ↑(Ideal.pi fun (x : ι) => Ideal.span {↑p ^ n})

Open and closed subgroups of ℤₚ

theorem PadicInt.denseRange_of_not_dvd (p : ℕ) [Fact (Nat.Prime p)] (a b : ℕ) (hb : ¬p ∣ b) : DenseRange fun (x : ℕ) => ↑a + ↑b * ↑x

theorem PadicInt.smul_mem_of_isClosed (p : ℕ) [Fact (Nat.Prime p)] (G : AddSubsemigroup ℤ_[p]) (hG : IsClosed ↑G) (c : ℤ_[p]) {x : ℤ_[p]} (hx : x ∈ G) : c • x ∈ G

theorem PadicInt.exists_eq_ideal_of_addSubsemigroup_of_isClosed (p : ℕ) [Fact (Nat.Prime p)] (G : AddSubsemigroup ℤ_[p]) (hne : (↑G).Nonempty) (hG : IsClosed ↑G) : ∃ (I : Ideal ℤ_[p]), G = I.toAddSubsemigroup

theorem PadicInt.exists_eq_ideal_of_addSubmonoid_of_isClosed (p : ℕ) [Fact (Nat.Prime p)] (G : AddSubmonoid ℤ_[p]) (hG : IsClosed ↑G) : ∃ (I : Ideal ℤ_[p]), G = I.toAddSubmonoid

theorem PadicInt.exists_eq_ideal_of_addSubgroup_of_isClosed (p : ℕ) [Fact (Nat.Prime p)] (G : AddSubgroup ℤ_[p]) (hG : IsClosed ↑G) : ∃ (I : Ideal ℤ_[p]), G = Submodule.toAddSubgroup I

theorem PadicInt.exists_eq_span_p_pow_of_isOpen (p : ℕ) [Fact (Nat.Prime p)] (G : AddSubgroup ℤ_[p]) (hG : IsOpen ↑G) : ∃ (n : ℕ), G = Submodule.toAddSubgroup (Ideal.span {↑p ^ n})