mathlib3

49ae0e37 - chore(topology/algebra/order/basic): move field-parts into new file (#17549)

chore(topology/algebra/order/basic): move field-parts into new file (#17549) File authorship credits go to: * Benjamin Davidson: #4138 * Devon Tuma: #7545 * Eric Rodriguez: #15022 * Oliver Nash: #16762