feat(RingTheory/LinearTopology): instance IsLinearTopology O R

[WenrongZou]

Let O, R be two rings. We define a type class predicate [IsIntegerSMul O R]: if the scalar multiplication of any element in O does not increase relative multiplication of R. And we prove an instance IsLinearTopology O R under the assumption of [IsIntegerSMul O R].

As a result, we have that IsLinearTopology ℤ_[p] ℤ_[p] and IsLinearTopology ℤ_[p] ℚ_[p].

• depends on: feat(ValuativeTopology): valuative topology of Z_p #43285

---

[github-actions]

PR summary 0ef599c318

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Padics.ValuativeRel	2312	2334	+22 (+0.95%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.Padics.ValuativeRel	22
Mathlib.Topology.Algebra.ValuativeRel.LinearTopology (new file)	2009
Mathlib.NumberTheory.Padics.LinearTopology (new file)	2336

---

Declarations diff (regex)

+ Integers.isIntegerSMul
+ Integers.of_compatible
+ IsIntegerRing
+ IsIntegerSMul
+ IsIntegerSMul.of_forall_smul_one_vle_one
+ _root_.Valuation.Integers.isLinearTopology
+ _root_.Valuation.Integers.isLinearTopology_self
+ instance : (mulValuation.comap (algebraMap ℤ_[p] ℚ_[p])).Compatible
+ instance : IsIntegerRing ℤ_[p]
+ instance : IsIntegerSMul (valuation R).integer R
+ instance : IsLinearTopology ℤ_[p] ℚ_[p] := inferInstance
+ instance : IsLinearTopology ℤ_[p] ℤ_[p] := inferInstance
+ instance : IsValuativeTopology ℤ_[p]
+ instance : ValuativeExtension ℤ_[p] ℚ_[p]
+ instance : ValuativeRel ℤ_[p]
+ instance [ValuativeRel.IsIntegerRing A] : IsIntegerSMul A B
+ integers
+ leSubmoduleOfSMulLe
+ leSubmoduleOfSMulLe_integer
+ leSubmoduleOfSMulLe_monotone
+ ltSubmoduleOfSMulLe
+ ltSubmoduleOfSMulLe_integer
+ ltSubmoduleOfSMulLe_le_leSubmoduleOfSMulLe
+ ltSubmoduleOfSMulLe_monotone
+ mem_leSubmoduleOfSMulLe_iff
+ mem_ltSubmoduleOfSMulLe_iff
+ mulValuation_le_one_iff_norm_le_one
+ of_integers
+ of_isIntegerSMul
+ of_isIntegerSMul_of_isInducing
+ of_valuation_smul_le
+ of_valuation_smul_le_of_isInducing
+ smul_le
+ smul_vle
+ valuation_integer_smul_le
+ valuation_le_one
+ valuation_le_one_iff_norm_le_one
+ valuation_smul_le
+ vle_one_iff_norm_le_one
+ vle_one_of_isIntegerRing

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 0ef599c).

• +45 new declarations
• −0 removed declarations

+IsLinearTopology.of_isIntegerSMul
+IsLinearTopology.of_isIntegerSMul_of_isInducing
+IsLinearTopology.of_valuation_smul_le
+IsLinearTopology.of_valuation_smul_le_of_isInducing
+IsValuativeTopology.of_integers
+Padic.instCompatiblePadicIntWithZeroMultiplicativeIntComapAlgebraMapMulValuation
+Padic.instIsValuativeTopologyPadicInt
+Padic.instValuativeExtensionPadicInt
+Padic.instValuativeRelPadicInt
+Padic.integers
+Padic.mulValuation_le_one_iff_norm_le_one
+Padic.valuation_le_one_iff_norm_le_one
+Padic.vle_one_iff_norm_le_one
+Valuation.Integers.isIntegerSMul
+Valuation.Integers.isLinearTopology
+Valuation.Integers.isLinearTopology_self
+Valuation.Integers.of_compatible
+Valuation.Integers.smul_le
+Valuation.instIsIntegerSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation
+Valuation.leSubmoduleOfSMulLe
+Valuation.leSubmoduleOfSMulLe_integer
+Valuation.leSubmoduleOfSMulLe_monotone
+Valuation.ltSubmoduleOfSMulLe
+Valuation.ltSubmoduleOfSMulLe_integer
+Valuation.ltSubmoduleOfSMulLe_le_leSubmoduleOfSMulLe
+Valuation.ltSubmoduleOfSMulLe_monotone
+Valuation.mem_leSubmoduleOfSMulLe_iff
+Valuation.mem_ltSubmoduleOfSMulLe_iff
+Valuation.valuation_integer_smul_le
+ValuativeExtension.instIsIntegerSMulOfIsIntegerRing
+ValuativeRel.IsIntegerRing
+ValuativeRel.IsIntegerSMul
+ValuativeRel.IsIntegerSMul.casesOn
+ValuativeRel.IsIntegerSMul.mk
+ValuativeRel.IsIntegerSMul.of_forall_smul_one_vle_one
+ValuativeRel.IsIntegerSMul.rec
+ValuativeRel.IsIntegerSMul.recOn
+ValuativeRel.IsIntegerSMul.smul_vle
+ValuativeRel.smul_vle
+ValuativeRel.valuation_le_one
+ValuativeRel.valuation_smul_le
+ValuativeRel.vle_one_of_isIntegerRing
+instIsIntegerRingPadicInt
+instIsLinearTopologyPadicInt
+instIsLinearTopologyPadicIntPadic

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5051	2

Current commit 0ef599c318
Reference commit 71a80585ee

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(ValuativeTopology): valuative topology of Z_p #43285
  By Dependent Issues (🤖). Happy coding!