| File | Mode | Size |
|---|---|---|
| adjoin.lean | -rw-r--r-- | 32.9 KB |
| admissible_absolute_value.lean | -rw-r--r-- | 20.8 KB |
| class_group.lean | -rw-r--r-- | 16.5 KB |
| class_number.lean | -rw-r--r-- | 21.7 KB |
| dedekind_domain.lean | -rw-r--r-- | 40.6 KB |
| defs.lean | -rw-r--r-- | 7.8 KB |
| fractional_ideal.lean | -rw-r--r-- | 41.6 KB |
| function_field.lean | -rw-r--r-- | 4.6 KB |
| integral_closure.lean | -rw-r--r-- | 26.4 KB |
| intermediate_field.lean | -rw-r--r-- | 15.1 KB |
| localization.lean | -rw-r--r-- | 68.2 KB |
| noetherian.lean | -rw-r--r-- | 29.8 KB |
| number_field.lean | -rw-r--r-- | 6.3 KB |
| power_basis.lean | -rw-r--r-- | 21.5 KB |
| primitive_element.lean | -rw-r--r-- | 11.0 KB |
| principal_ideal_domain.lean | -rw-r--r-- | 10.0 KB |
| subfield.lean | -rw-r--r-- | 23.8 KB |
| trace.lean | -rw-r--r-- | 52.9 KB |
| unique_factorization_domain.lean | -rw-r--r-- | 51.3 KB |
