Skip to content

[Merged by Bors] - feat: AbsoluteValue.IsNontrivial#20588

Closed
MichaelStollBayreuth wants to merge 2 commits intomasterfrom
MS_AbsValue_isNontrivial
Closed

[Merged by Bors] - feat: AbsoluteValue.IsNontrivial#20588
MichaelStollBayreuth wants to merge 2 commits intomasterfrom
MS_AbsValue_isNontrivial

Conversation

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth commented Jan 8, 2025

This introduces v.IsNontrivial : Prop for v : AbsoluteValue R S; this states that v x ≠ 1 for some x ≠ 0.

This is more convenient to use than v ≠ .trivial since it does not require additional assumptions on R or S (whereas AbsoluteValue.trivial needs x = 0 to be decidable in R, R to have no zero divisors and S to be nontrivial).

We also adapt NumberTheory.Ostrowski to use IsNontrivial instead of ≠ .trivial.

Open in Gitpod

@MichaelStollBayreuth MichaelStollBayreuth added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-analysis Analysis (normed *, calculus) labels Jan 8, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 8, 2025 •
edited
Loading

PR summary 78a8741662

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsNontrivial
+ IsNontrivial.exists_abv_gt_one
+ IsNontrivial.exists_abv_lt_one
+ isNontrivial_iff_ne_trivial
+ not_isNontrivial_apply
+ not_isNontrivial_iff

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh 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).

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 8, 2025
jcommelin
jcommelin reviewed Jan 10, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 10, 2025

✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 10, 2025
@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor Author

MichaelStollBayreuth commented Jan 10, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 10, 2025
@MichaelStollBayreuth
feat: AbsoluteValue.IsNontrivial (#20588)
e6e7902 
This introduces `v.IsNontrivial : Prop` for `v : AbsoluteValue R S`; this states that `v x  ≠ 1` for some `x ≠ 0`.

This is more convenient to use than `v ≠ .trivial` since it does not require additional assumptions on `R` or `S` (whereas `AbsoluteValue.trivial` needs `x = 0` to be decidable in `R`, `R` to have no zero divisors and `S` to be nontrivial).

We also adapt `NumberTheory.Ostrowski` to use `IsNontrivial` instead of `≠ .trivial`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: AbsoluteValue.IsNontrivial [Merged by Bors] - feat: AbsoluteValue.IsNontrivial Jan 10, 2025
@mathlib-bors mathlib-bors bot closed this Jan 10, 2025
@mathlib-bors mathlib-bors bot deleted the MS_AbsValue_isNontrivial branch January 10, 2025 11:46
grunweg pushed a commit that referenced this pull request Jan 11, 2025
@MichaelStollBayreuth @grunweg
feat: AbsoluteValue.IsNontrivial (#20588)
da5130d 
This introduces `v.IsNontrivial : Prop` for `v : AbsoluteValue R S`; this states that `v x  ≠ 1` for some `x ≠ 0`.

This is more convenient to use than `v ≠ .trivial` since it does not require additional assumptions on `R` or `S` (whereas `AbsoluteValue.trivial` needs `x = 0` to be decidable in `R`, `R` to have no zero divisors and `S` to be nontrivial).

We also adapt `NumberTheory.Ostrowski` to use `IsNontrivial` instead of `≠ .trivial`.
Julian added a commit that referenced this pull request Jan 12, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
9ba6079 
* origin/master: (88 commits)
  chore(scripts): update nolints.json (#20672)
  chore: de-simp `map_eq_zero_iff_eq_one` (#20662)
  feat(Combinatorics/SimpleGraph): add independent sets (#18608)
  chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641)
  feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366)
  feat(AlgebraicTopology): model categories (#19158)
  chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548)
  feat(Data/List/ReduceOption): add replicate theorems (#20644)
  feat: approximate subgroups (#20050)
  feat: use scoped trace nodes in linarith (#19855)
  feat: disjoint union of charted spaces (#20619)
  feat: add some term elaborators for reduction (#15192)
  feat(Topology/Category): category of delta-generated spaces (#19499)
  add a variable_alias for Quantale and AddQuantale (#19282)
  feat(Computability/DFA): implement `isRegular_iff` (#19940)
  chore: unpin and bump batteries and importgraph (#20651)
  chore: split `Mathlib/Algebra/Group/Int` (#20624)
  feat: three lemmas related to Hausdorff distance (#20585)
  chore: `initialize_simps_projections` for `Submodule` (#20582)
  feat(Order): Boolean algebra structure on idempotents (#20618)
  chore(CategoryTheory): moving/renaming Subpresheaf (#20583)
  refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630)
  feat: sets of doubling strictly less than 3/2 (#20572)
  chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452)
  feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298)
  feat: product of subalgebras (#20202)
  feat: `Submodule.restrictScalars` commutes with `pow` (#20581)
  feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580)
  chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576)
  chore: use ofNat more (#20546)
  feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363)
  feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797)
  refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590)
  feat: Make `PNat.recOn` induction eliminator (#20617)
  feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608)
  feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574)
  feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573)
  chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611)
  feat: AbsoluteValue.IsNontrivial (#20588)
  chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092)
  chore(Data/Set): split the `CoeSort` instance to its own file (#19031)
  feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612)
  feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286)
  chore: cleanup more `erw` (#20601)
  chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587)
  chore: cleanup imports in PrimePow/Divisors (#20626)
  chore: split Algebra/BigOperators/Group/List (#20625)
  chore: reduce Topology->Order imports by moving content (#20627)
  chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592)
  refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@MichaelStollBayreuth @jcommelin