leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

756bd9d7

eric-wieser committed 3 years ago

dacdffde

eric-wieser committed 3 years ago

68c2af21

chore(ring_theory/graded_algebra/basic): add homogeneous_decompose

eric-wieser committed 3 years ago

f189e191

jjaassoonn committed 3 years ago

28b526ed

jjaassoonn committed 3 years ago

d64fc9b0

jjaassoonn committed 3 years ago

7f634dfa

moved homogeneous_core upfront, changed definition

jjaassoonn committed 3 years ago

020c8755

Update src/ring_theory/graded_algebra/homogeneous_ideal.lean

jjaassoonn committed 3 years ago

Verified 5184dc95

Update homogeneous_ideal.lean

jjaassoonn committed 3 years ago

Verified 3e579e70

jjaassoonn committed 3 years ago

Verified f336c03e

jjaassoonn committed 3 years ago

7a5af877

remove noncomputable

jjaassoonn committed 3 years ago

aeed44b0

jjaassoonn committed 3 years ago

07fa56c5

Merge branch 'homogeneous_ideal_easier_part' of https://github.com/leanprover-community/mathlib into homogeneous_ideal_easier_part

jjaassoonn committed 3 years ago

067e3d8a

rollback to old defs

jjaassoonn committed 3 years ago

ac712726

Update src/ring_theory/graded_algebra/homogeneous_ideal.lean

jjaassoonn committed 4 years ago

Verified bf71110e

jjaassoonn committed 4 years ago

8d7b6b59

Merge branch 'homogeneous_ideal_easier_part' of https://github.com/leanprover-community/mathlib into homogeneous_ideal_easier_part

jjaassoonn committed 4 years ago

a0e12949

galois coinsertion

jjaassoonn committed 4 years ago

38489492

Apply suggestions from code review

jjaassoonn committed 4 years ago

Verified 5da9acb2

jjaassoonn committed 4 years ago

8c8fe55c

changed submodule R R to ideal R

jjaassoonn committed 4 years ago

e96193c6

delete unused argument

jjaassoonn committed 4 years ago

90e16ffb

add `homogeneous_hull.eq_Inf`

jjaassoonn committed 4 years ago

0d76863f

jjaassoonn committed 4 years ago

7bbdbbd3

apply suggestion

jjaassoonn committed 4 years ago

664e2514

`lemma ideal.homogenisation.eq_Sup [Π (i : ι) (x : A i), decidable (x ≠ 0)] `

jjaassoonn committed 4 years ago

a6b1f1c6

jjaassoonn committed 4 years ago

de2e8a3f

homogenisation is mono

jjaassoonn committed 4 years ago

f51fbeef

Older