Search results

feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 27114

#27114 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

feat(RingTheory/SimpleRing/Principal): a simple ring is a PID

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27113

#27113 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

feat(GroupTheory/ArchimedeanDensely) <code>Int.set_denselyOrdered_iff_subsingleton</code>

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 27112

#27112 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

chore(RingTheory/ValuationSubring): valuationSubring_integers

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

Status: Open (in progress).

leanprover-community/mathlib4number 27111

#27111 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

chore(Valued/WithVal): apply_symm_equiv

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 27110

#27110 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

feat(RingTheory/AdicValuation): valuation_surjective

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

Status: Open (in progress).

leanprover-community/mathlib4number 27109

#27109 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

chore(RingTheory/AdicValuation): golf using WithZero.log

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

Status: Open (in progress).

leanprover-community/mathlib4number 27108

#27108 In leanprover-community/mathlib4;

· pechersky opened on Jul 14, 2025

feat(GroupTheory/GroupAction/SubMulAction/Combination) : combinations and group actions

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27107

#27107 In leanprover-community/mathlib4;

· AntoineChambert-Loir opened on Jul 14, 2025

feat(Ring/DedekindDomain): formula for the splitting of primes in extension

large-importAutomatically added label for PRs with a significant increase in transitive importsAutomatically added label for PRs with a significant increase in transitive imports

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27105

#27105 In leanprover-community/mathlib4;

· xroblot opened on Jul 14, 2025

feat: semilinearize <code>LinearEquiv.conjRingEquiv</code>

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27104

#27104 In leanprover-community/mathlib4;

· eric-wieser opened on Jul 13, 2025

feat(Algebra/Category/ModuleCat/Sheaf/VectorBundle): define vector bundles

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27098

#27098 In leanprover-community/mathlib4;

· Paul-Lez opened on Jul 13, 2025

feat(LinearAlgebra/Finsupp/LinearCombination): add <code>Submodule.mem_span_finset'</code>

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27097

#27097 In leanprover-community/mathlib4;

· staroperator opened on Jul 13, 2025