Theorem IntermediateField.finrank_bot'

Modification history

2026-03-17 23:30

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

chore: mark `toSubfield`, `toSubmodule`, `toSubring` as `reducible` (#36395) …

Modified IntermediateField.finrank_bot'View on Github →

2024-02-23 22:33

Mathlib/FieldTheory/Adjoin.lean

feat(FieldTheory/Adjoin): add `IntermediateField.[fin]rank_bot'` (#10896)

Added IntermediateField.finrank_bot'View on Github →